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