Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified syntax -- to make it work for authentic syntax;
authorwenzelm
Sun, 21 Feb 2010 20:54:40 +0100
changeset 35252 24c466b2cdc8
parent 35251 e244adbbc28f
child 35253 68dd8b51c6b8
simplified syntax -- to make it work for authentic syntax;
src/Sequents/ILL_predlog.thy file | annotate | diff | comparison | revisions 
--- 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*]"
isabelle