--- a/src/HOL/IMP/Procs.thy Fri May 17 02:57:00 2013 +0200
+++ b/src/HOL/IMP/Procs.thy Fri May 17 08:19:52 2013 +0200
@@ -9,20 +9,20 @@
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)
- | Var vname com ("(1{VAR _;;/ _})")
- | Proc pname com com ("(1{PROC _ = _;;/ _})")
+ | Var vname com ("(1{VAR _;/ _})")
+ | Proc pname com com ("(1{PROC _ = _;/ _})")
| CALL pname
definition "test_com =
-{VAR ''x'';;
- {PROC ''p'' = ''x'' ::= N 1;;
- {PROC ''q'' = CALL ''p'';;
- {VAR ''x'';;
- ''x'' ::= N 2;
- {PROC ''p'' = ''x'' ::= N 3;;
- CALL ''q''; ''y'' ::= V ''x''}}}}}"
+{VAR ''x'';
+ {PROC ''p'' = ''x'' ::= N 1;
+ {PROC ''q'' = CALL ''p'';
+ {VAR ''x'';
+ ''x'' ::= N 2;;
+ {PROC ''p'' = ''x'' ::= N 3;
+ CALL ''q'';; ''y'' ::= V ''x''}}}}}"
end