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)