1.1 --- a/src/HOL/IMP/Procs.thy	Sun Feb 03 17:31:33 2013 +0100
     1.2 +++ b/src/HOL/IMP/Procs.thy	Mon Feb 04 09:06:20 2013 +0100
     1.3 @@ -18,12 +18,11 @@
     1.4  
     1.5  definition "test_com =
     1.6  {VAR ''x'';;
     1.7 - ''x'' ::= N 0;
     1.8 - {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
     1.9 + {PROC ''p'' = ''x'' ::= N 1;;
    1.10    {PROC ''q'' = CALL ''p'';;
    1.11     {VAR ''x'';;
    1.12 -    ''x'' ::= N 5;
    1.13 -    {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
    1.14 +    ''x'' ::= N 2;
    1.15 +    {PROC ''p'' = ''x'' ::= N 3;;
    1.16       CALL ''q''; ''y'' ::= V ''x''}}}}}"
    1.17  
    1.18  end

     2.1 --- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Sun Feb 03 17:31:33 2013 +0100
     2.2 +++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Mon Feb 04 09:06:20 2013 +0100
     2.3 @@ -31,9 +31,6 @@
     2.4  
     2.5  code_pred big_step .
     2.6  
     2.7 -values "{map t [''x'',''y'',''z''] |t. 
     2.8 -          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
     2.9 -
    2.10 -values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
    2.11 +values "{map t [''x'',''y''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
    2.12  
    2.13  end

     3.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Sun Feb 03 17:31:33 2013 +0100
     3.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Mon Feb 04 09:06:20 2013 +0100
     3.3 @@ -33,9 +33,6 @@
     3.4  
     3.5  code_pred big_step .
     3.6  
     3.7 -values "{map t [''x'', ''y'', ''z''] |t. 
     3.8 -            [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
     3.9 -
    3.10 -values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
    3.11 +values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
    3.12  
    3.13  end

     4.1 --- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Sun Feb 03 17:31:33 2013 +0100
     4.2 +++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Mon Feb 04 09:06:20 2013 +0100
     4.3 @@ -32,7 +32,7 @@
     4.4     e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
     4.5  
     4.6  Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>
     4.7 -      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
     4.8 +      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
     4.9  
    4.10  Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>
    4.11          ((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
    4.12 @@ -45,10 +45,8 @@
    4.13  code_pred big_step .
    4.14  
    4.15  
    4.16 -values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
    4.17 -
    4.18 -values "{map t [0, 1, 2] |t.
    4.19 -  ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
    4.20 +values "{map t [10,11] |t.
    4.21 +  ([], <''x'' := 10, ''y'' := 11>, 12)
    4.22    \<turnstile> (test_com, <>) \<Rightarrow> t}"
    4.23  
    4.24  end