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