src/HOL/Hoare/hoare_tac.ML
changeset 37138 ee23611b6bf2
parent 37135 636e6d8645d6
child 37391 476270a6c2dc
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:17:30 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed May 26 16:28:55 2010 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4  val before_set2pred_simp_tac =
     1.5    (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
     1.6  
     1.7 -val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
     1.8 +val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]));
     1.9  
    1.10  (*****************************************************************************)
    1.11  (** set2pred_tac transforms sets inclusion into predicates implication,     **)
    1.12 @@ -111,7 +111,7 @@
    1.13      rtac CollectI i,
    1.14      dtac CollectD i,
    1.15      TRY (split_all_tac i) THEN_MAYBE
    1.16 -     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)]);
    1.17 +     (rename_tac var_names i THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_conv}]) i)]);
    1.18  
    1.19  (*****************************************************************************)
    1.20  (** BasicSimpTac is called to simplify all verification conditions. It does **)
    1.21 @@ -125,7 +125,7 @@
    1.22  
    1.23  fun BasicSimpTac var_names tac =
    1.24    simp_tac
    1.25 -    (HOL_basic_ss addsimps [mem_Collect_eq, split_conv] addsimprocs [record_simproc])
    1.26 +    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
    1.27    THEN_MAYBE' MaxSimpTac var_names tac;
    1.28  
    1.29