src/HOL/Bali/AxExample.thy
 changeset 14030 cd928c0ac225 parent 13688 a0b16d42d489 child 14981 e73f8140af78
```--- 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" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> hd vs = Null) \<and>. heap_free two)" *})
+apply     (tactic {* inst1_tac "R14" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. 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" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
+apply   (tactic {* inst1_tac "P'34" "\<lambda>u a. Normal (?PP a\<leftarrow>?x) u" *})
apply   (simp (no_asm) del: peek_and_def2)
apply   (tactic "ax_tac 1")
prefer 2```