# HG changeset patch # User berghofe # Date 1210150760 -7200 # Node ID 255a347eae4379a0601747915904d798019875dd # Parent da662ff93503f099207e4e06ae2d470331266086 Locally deleted some definitions that were applied too eagerly because of eta-expansion diff -r da662ff93503 -r 255a347eae43 src/HOL/Bali/AxExample.thy --- 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'" "\a vs l vf. ?PP a vs l vf\?x \. ?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'" "\u a. Normal (?PP a\?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'" "\aa v. Normal (?QQ aa v\?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'" "\u vf. Normal (?PP vf \. ?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'" "\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")