Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/IMP/Com.thy
changeset 19796 d86e7b1fc472
parent 16417 9bc16273c2d4
child 22808 a7daa74e2980 
--- a/src/ZF/IMP/Com.thy	Tue Jun 06 19:24:05 2006 +0200
+++ b/src/ZF/IMP/Com.thy	Tue Jun 06 20:42:25 2006 +0200
@@ -78,7 +78,7 @@
   | assignment ("x \<in> loc", "a \<in> aexp")       (infixl "\<ASSN>" 60)
   | semicolon ("c0 \<in> com", "c1 \<in> com")       ("_\<SEQ> _"  [60, 60] 10)
   | while ("b \<in> bexp", "c \<in> com")            ("\<WHILE> _ \<DO> _"  60)
-  | if ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
+  | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com")    ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
 
 
 consts evalc :: i
isabelle