src/Sequents/ILL_predlog.thy

 consts
   conj :: "[plf,plf] => plf"   (infixr "&" 35)
   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)
 
 syntax
   "_NG" :: "plf => plf"   ("- _ " [50] 55)
 
 translations
 
   "[* 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*]"
 
 (* another translations for linear implication: