# HG changeset patch
# User wenzelm
# Date 1177598354 -7200
# Node ID c0695a818c091ba14437021e8a180584665daea0
# Parent  9dfadec17cc41e3d5f6c3229c01d02b7a3696a84
eliminated unnamed infixes;

diff -r 9dfadec17cc4 -r c0695a818c09 src/HOL/IMP/Expr.thy
--- 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"