dropped legacy theorem bindings
authorhaftmann
Wed May 26 16:28:55 2010 +0200 (2010-05-26)
changeset 37138ee23611b6bf2
parent 37137 bac3d00a910a
child 37139 e0bd5934a2fb
dropped legacy theorem bindings
src/HOL/Bali/AxExample.thy
src/HOL/Hoare/hoare_tac.ML
     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")
     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:17:30 2010 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:28:55 2010 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4  val before_set2pred_simp_tac =
     2.5    (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
     2.6  
     2.7 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
     2.8 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
     2.9  
    2.10  (*****************************************************************************)
    2.11  (** set2pred_tac transforms sets inclusion into predicates implication,     **)
    2.12 @@ -111,7 +111,7 @@
    2.13      rtac CollectI i,
    2.14      dtac CollectD i,
    2.15      TRY (split_all_tac i) THEN_MAYBE
    2.16 -     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
    2.17 +     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
    2.18  
    2.19  (*****************************************************************************)
    2.20  (** BasicSimpTac is called to simplify all verification conditions. It does **)
    2.21 @@ -125,7 +125,7 @@
    2.22  
    2.23  fun BasicSimpTac var_names tac =
    2.24    simp_tac
    2.25 -    (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
    2.26 +    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
    2.27    THEN_MAYBE' MaxSimpTac var_names tac;
    2.28  
    2.29