diff -r a4a32c1d2866 -r 146f63c3f024 src/HOL/IMP/Procs.thy --- a/src/HOL/IMP/Procs.thy Sun Feb 03 17:31:33 2013 +0100 +++ b/src/HOL/IMP/Procs.thy Mon Feb 04 09:06:20 2013 +0100 @@ -18,12 +18,11 @@ definition "test_com = {VAR ''x'';; - ''x'' ::= N 0; - {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');; + {PROC ''p'' = ''x'' ::= N 1;; {PROC ''q'' = CALL ''p'';; {VAR ''x'';; - ''x'' ::= N 5; - {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);; + ''x'' ::= N 2; + {PROC ''p'' = ''x'' ::= N 3;; CALL ''q''; ''y'' ::= V ''x''}}}}}" end