| 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*]"