# HG changeset patch
# User nipkow
# Date 1359965180 -3600
# Node ID 146f63c3f024fe2ca99e15b4705a7329ac4daa86
# Parent  a4a32c1d2866d899df7ac49b338e3083da044896
tuned

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
diff -r a4a32c1d2866 -r 146f63c3f024 src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy	Mon Feb 04 09:06:20 2013 +0100
@@ -31,9 +31,6 @@
 
 code_pred big_step .
 
-values "{map t [''x'',''y'',''z''] |t. 
-          (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'',''y''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end
diff -r a4a32c1d2866 -r 146f63c3f024 src/HOL/IMP/Procs_Stat_Vars_Dyn.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy	Mon Feb 04 09:06:20 2013 +0100
@@ -33,9 +33,6 @@
 
 code_pred big_step .
 
-values "{map t [''x'', ''y'', ''z''] |t. 
-            [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end
diff -r a4a32c1d2866 -r 146f63c3f024 src/HOL/IMP/Procs_Stat_Vars_Stat.thy
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy	Mon Feb 04 09:06:20 2013 +0100
@@ -32,7 +32,7 @@
    e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
 
 Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t  \<Longrightarrow>
-      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
+      (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
 
 Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t  \<Longrightarrow>
         ((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
@@ -45,10 +45,8 @@
 code_pred big_step .
 
 
-values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
-
-values "{map t [0, 1, 2] |t.
-  ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
+values "{map t [10,11] |t.
+  ([], <''x'' := 10, ''y'' := 11>, 12)
   \<turnstile> (test_com, <>) \<Rightarrow> t}"
 
 end