diff -r 90cd3c53a887 -r bc01725d7918 src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Fri May 17 02:57:00 2013 +0200 +++ b/src/HOL/IMP/Com.thy Fri May 17 08:19:52 2013 +0200 @@ -5,7 +5,7 @@ datatype com = SKIP | Assign vname aexp ("_ ::= _" [1000, 61] 61) - | Seq com com ("_;/ _" [60, 61] 60) + | Seq com com ("_;;/ _" [60, 61] 60) | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | While bexp com ("(WHILE _/ DO _)" [0, 61] 61)