--- a/src/HOL/Bali/AxExample.thy Wed May 07 10:59:19 2008 +0200
+++ b/src/HOL/Bali/AxExample.thy Wed May 07 10:59:20 2008 +0200
@@ -136,7 +136,7 @@
apply (rule ax_subst_Var_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>a vs l vf. ?PP a vs l vf\<leftarrow>?x \<and>. ?p" *})
apply (rule allI)
-apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [thm "peek_and_def2"]) 1 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
apply (rule ax_derivs.Abrupt)
apply (simp (no_asm))
apply (tactic "ax_tac 1" (* FVar *))
@@ -148,12 +148,12 @@
apply (rule ax_derivs.Done [THEN conseq1],force)
apply (rule ax_subst_Val_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
-apply (simp (no_asm) del: peek_and_def2)
+apply (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply (tactic "ax_tac 1")
prefer 2
apply (rule ax_subst_Val_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>aa v. Normal (?QQ aa v\<leftarrow>?y)" *})
-apply (simp del: peek_and_def2)
+apply (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
@@ -172,7 +172,7 @@
defer
apply (rule ax_subst_Var_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>u vf. Normal (?PP vf \<and>. ?p) u" *})
-apply (simp (no_asm) del: split_paired_All peek_and_def2)
+apply (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply (tactic "ax_tac 1" (* NewC *))
apply (tactic "ax_tac 1" (* ax_Alloc *))
(* just for clarification: *)
@@ -200,7 +200,7 @@
apply (tactic "ax_tac 1")
apply (rule_tac [2] ax_subst_Var_allI)
apply (tactic {* inst1_tac "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
-apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, thm "peek_and_def2"]) 2 *})
+apply (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [split_paired_All, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply (tactic "ax_tac 2" (* NewA *))
apply (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply (tactic "ax_tac 3")