changeset 22818 | c0695a818c09 |
parent 20503 | 503ac4c5ef91 |
child 23746 | a455e69c31cc |
--- a/src/HOL/IMP/Expr.thy Thu Apr 26 16:39:11 2007 +0200 +++ b/src/HOL/IMP/Expr.thy Thu Apr 26 16:39:14 2007 +0200 @@ -48,8 +48,8 @@ | false | ROp "nat => nat => bool" aexp aexp | noti bexp - | andi bexp bexp (infixl 60) - | ori bexp bexp (infixl 60) + | andi bexp bexp (infixl "andi" 60) + | ori bexp bexp (infixl "ori" 60) subsection "Evaluation of boolean expressions" consts evalb :: "((bexp*state) * bool)set"