src/HOL/Induct/Com.thy
changeset 3146 922a60451382
parent 3120 c58423c20740
child 4264 5e21f41ccd21
--- a/src/HOL/Induct/Com.thy	Fri May 09 10:17:41 1997 +0200
+++ b/src/HOL/Induct/Com.thy	Fri May 09 10:18:07 1997 +0200
@@ -23,7 +23,7 @@
       | valOf exp exp          ("VALOF _ RESULTIS _"  60)
       | SKIP
       | ":="  loc exp          (infixl  60)
-      | Semi  exp exp          ("_;;_"  [60, 60] 10)
+      | Semi  exp exp          ("_;;_"  [60, 60] 60)
       | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
       | While exp exp          ("WHILE _ DO _"  60)