diff -r fe031a7c75bc -r cd928c0ac225 src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Wed May 14 15:22:37 2003 +0200 +++ b/src/HOL/Bali/AxExample.thy Wed May 14 20:29:18 2003 +0200 @@ -130,12 +130,12 @@ apply (tactic "ax_tac 1" (* FVar *)) apply (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2") apply (tactic "ax_tac 1") -apply (tactic {* inst1_tac "R14" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ hd vs = Null) \. heap_free two)" *}) +apply (tactic {* inst1_tac "R14" "\a'. Normal ((\Vals:vs (x, s) Z. arr_inv s \ inited Ext (globs s) \ a' \ Null \ vs = [Null]) \. heap_free two)" *}) apply fastsimp prefer 4 apply (rule ax_derivs.Done [THEN conseq1],force) apply (rule ax_subst_Val_allI) -apply (tactic {* inst1_tac "P'33" "\u a. Normal (?PP a\?x) u" *}) +apply (tactic {* inst1_tac "P'34" "\u a. Normal (?PP a\?x) u" *}) apply (simp (no_asm) del: peek_and_def2) apply (tactic "ax_tac 1") prefer 2