src/ZF/IMP/Com.thy
changeset 22808 a7daa74e2980
parent 19796 d86e7b1fc472
child 35068 544867142ea4
--- a/src/ZF/IMP/Com.thy	Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/IMP/Com.thy	Thu Apr 26 14:24:08 2007 +0200
@@ -45,8 +45,8 @@
        | false
        | ROp  ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
        | noti ("b \<in> bexp")
-       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
-       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl 60)
+       | andi ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "andi" 60)
+       | ori  ("b0 \<in> bexp", "b1 \<in> bexp")      (infixl "ori" 60)
 
 
 consts evalb :: i