src/HOL/Bali/AxExample.thy
changeset 37138 ee23611b6bf2
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/AxExample.thy	Wed May 26 16:17:30 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Wed May 26 16:28:55 2010 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4  apply     (tactic "ax_tac 1")
     1.5  apply     (rule_tac [2] ax_subst_Var_allI)
     1.6  apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (?P vf l vfa)" *})
     1.7 -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 *})
     1.8 +apply     (tactic {* simp_tac (@{simpset} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
     1.9  apply      (tactic "ax_tac 2" (* NewA *))
    1.10  apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
    1.11  apply       (tactic "ax_tac 3")