# HG changeset patch
# User wenzelm
# Date 1266782080 -3600
# Node ID 24c466b2cdc83f74ea856d0978c37d6aa84efef8
# Parent  e244adbbc28fa24e5967a3d2fa542f5a1a0b3833
simplified syntax -- to make it work for authentic syntax;

diff -r e244adbbc28f -r 24c466b2cdc8 src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Sun Feb 21 20:54:07 2010 +0100
+++ b/src/Sequents/ILL_predlog.thy	Sun Feb 21 20:54:40 2010 +0100
@@ -11,7 +11,7 @@
   disj :: "[plf,plf] => plf"   (infixr "|" 35)
   impl :: "[plf,plf] => plf"   (infixr ">" 35)
   eq :: "[plf,plf] => plf"   (infixr "=" 35)
-  ff    :: "plf"
+  ff :: "plf"    ("ff")
 
   PL    :: "plf => o"      ("[* / _ / *]" [] 100)
 
@@ -22,8 +22,8 @@
 
   "[* A & B *]" == "[*A*] && [*B*]"
   "[* A | B *]" == "![*A*] ++ ![*B*]"
-  "[* - A *]"   == "[*A > CONST ff*]"
-  "[* XCONST ff *]" == "0"
+  "[* - A *]" == "[*A > ff*]"
+  "[* ff *]" == "0"
   "[* A = B *]" => "[* (A > B) & (B > A) *]"
 
   "[* A > B *]" == "![*A*] -o [*B*]"