--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ex/ILL/ILL_predlog.thy Wed Oct 09 13:32:33 1996 +0200
@@ -0,0 +1,42 @@
+(*
+ File: /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
+ Theory Name: pred_log
+ Logic Image: HOL
+*)
+
+ILL_predlog = ILL +
+
+types
+
+ plf
+
+arities
+
+ plf :: logic
+
+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