eliminated unnamed infixes;
authorwenzelm
Thu Apr 26 16:39:14 2007 +0200 (2007-04-26)
changeset 22818c0695a818c09
parent 22817 9dfadec17cc4
child 22819 a7b425bb668c
eliminated unnamed infixes;
src/HOL/IMP/Expr.thy
     1.1 --- a/src/HOL/IMP/Expr.thy	Thu Apr 26 16:39:11 2007 +0200
     1.2 +++ b/src/HOL/IMP/Expr.thy	Thu Apr 26 16:39:14 2007 +0200
     1.3 @@ -48,8 +48,8 @@
     1.4         | false
     1.5         | ROp  "nat => nat => bool" aexp aexp
     1.6         | noti bexp
     1.7 -       | andi bexp bexp         (infixl 60)
     1.8 -       | ori  bexp bexp         (infixl 60)
     1.9 +       | andi bexp bexp         (infixl "andi" 60)
    1.10 +       | ori  bexp bexp         (infixl "ori" 60)
    1.11  
    1.12  subsection "Evaluation of boolean expressions"
    1.13  consts evalb    :: "((bexp*state) * bool)set"