src/Sequents/ILL_predlog.thy
changeset 35054 a5db9779b026
parent 22895 adc529c89281
child 35252 24c466b2cdc8
     1.1 --- a/src/Sequents/ILL_predlog.thy	Wed May 09 19:37:20 2007 +0200
     1.2 +++ b/src/Sequents/ILL_predlog.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -22,8 +22,8 @@
     1.4  
     1.5    "[* A & B *]" == "[*A*] && [*B*]"
     1.6    "[* A | B *]" == "![*A*] ++ ![*B*]"
     1.7 -  "[* - A *]"   == "[*A > ff*]"
     1.8 -  "[* ff *]"    == "0"
     1.9 +  "[* - A *]"   == "[*A > CONST ff*]"
    1.10 +  "[* XCONST ff *]" == "0"
    1.11    "[* A = B *]" => "[* (A > B) & (B > A) *]"
    1.12  
    1.13    "[* A > B *]" == "![*A*] -o [*B*]"