Up to index of Isabelle/Sequents/ILL
theory ILL_predlog(* $Id: ILL_predlog.thy,v 1.3 2005/09/18 13:20:10 wenzelm Exp $ *) theory ILL_predlog imports ILL begin typedecl plf consts "&" :: "[plf,plf] => plf" (infixr 35) "|" :: "[plf,plf] => plf" (infixr 35) ">" :: "[plf,plf] => plf" (infixr 35) "=" :: "[plf,plf] => plf" (infixr 35) "@NG" :: "plf => plf" ("- _ " [50] 55) ff :: "plf" PL :: "plf => o" ("[* / _ / *]" [] 100) translations "[* A & B *]" == "[*A*] && [*B*]" "[* A | B *]" == "![*A*] ++ ![*B*]" "[* - A *]" == "[*A > ff*]" "[* ff *]" == "0" "[* A = B *]" => "[* (A > B) & (B > A) *]" "[* A > B *]" == "![*A*] -o [*B*]" (* another translations for linear implication: "[* A > B *]" == "!([*A*] -o [*B*])" *) end