Locally deleted some definitions that were applied too eagerly because
of eta-expansion

--- 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")