changeset 35054 | a5db9779b026 |
parent 22895 | adc529c89281 |
child 35252 | 24c466b2cdc8 |
--- a/src/Sequents/ILL_predlog.thy Mon Feb 08 21:26:52 2010 +0100 +++ b/src/Sequents/ILL_predlog.thy Mon Feb 08 21:28:27 2010 +0100 @@ -22,8 +22,8 @@ "[* A & B *]" == "[*A*] && [*B*]" "[* A | B *]" == "![*A*] ++ ![*B*]" - "[* - A *]" == "[*A > ff*]" - "[* ff *]" == "0" + "[* - A *]" == "[*A > CONST ff*]" + "[* XCONST ff *]" == "0" "[* A = B *]" => "[* (A > B) & (B > A) *]" "[* A > B *]" == "![*A*] -o [*B*]"