src/Sequents/ILL/ILL_predlog.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ILL/ILL_predlog.thy	Fri Feb 05 21:14:17 1999 +0100
@@ -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