eliminated change_claset/simpset;
authorwenzelm
Wed Mar 19 22:47:35 2008 +0100 (2008-03-19)
changeset 263397825c83c9eff
parent 26338 f8ed02f22433
child 26340 a85fe32e7b2f
eliminated change_claset/simpset;
src/HOL/Datatype.thy
src/HOL/Set.thy
src/HOLCF/HOLCF.thy
src/HOLCF/IOA/NTP/Correctness.thy
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.thy
src/ZF/Main_ZF.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/HOL/Datatype.thy	Wed Mar 19 22:28:17 2008 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Mar 19 22:47:35 2008 +0100
     1.3 @@ -635,7 +635,9 @@
     1.4  lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
     1.5    by simp
     1.6  
     1.7 -ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
     1.8 +declaration {* fn _ =>
     1.9 +  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
    1.10 +*}
    1.11  
    1.12  lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
    1.13    by (cases xo) auto
     2.1 --- a/src/HOL/Set.thy	Wed Mar 19 22:28:17 2008 +0100
     2.2 +++ b/src/HOL/Set.thy	Wed Mar 19 22:47:35 2008 +0100
     2.3 @@ -428,8 +428,8 @@
     2.4    Gives better instantiation for bound:
     2.5  *}
     2.6  
     2.7 -ML_setup {*
     2.8 -  change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
     2.9 +declaration {* fn _ =>
    2.10 +  Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
    2.11  *}
    2.12  
    2.13  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
    2.14 @@ -1031,9 +1031,11 @@
    2.15     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
    2.16   *)
    2.17  
    2.18 -ML_setup {*
    2.19 +ML {*
    2.20    val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
    2.21 -  change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    2.22 +*}
    2.23 +declaration {* fn _ =>
    2.24 +  Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs))
    2.25  *}
    2.26  
    2.27  
     3.1 --- a/src/HOLCF/HOLCF.thy	Wed Mar 19 22:28:17 2008 +0100
     3.2 +++ b/src/HOLCF/HOLCF.thy	Wed Mar 19 22:47:35 2008 +0100
     3.3 @@ -21,8 +21,8 @@
     3.4  
     3.5  defaultsort pcpo
     3.6  
     3.7 -ML_setup {*
     3.8 -  change_simpset (fn simpset => simpset addSolver
     3.9 +declaration {* fn _ =>
    3.10 +  Simplifier.map_ss (fn simpset => simpset addSolver
    3.11      (mk_solver' "adm_tac" (fn ss =>
    3.12        adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
    3.13  *}
     4.1 --- a/src/HOLCF/IOA/NTP/Correctness.thy	Wed Mar 19 22:28:17 2008 +0100
     4.2 +++ b/src/HOLCF/IOA/NTP/Correctness.thy	Wed Mar 19 22:47:35 2008 +0100
     4.3 @@ -14,9 +14,9 @@
     4.4    "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
     4.5                           else tl(sq(sen s)))"
     4.6  
     4.7 -ML_setup {*
     4.8 -(* repeated from Traces.ML *)
     4.9 -change_claset (fn cs => cs delSWrapper "split_all_tac")
    4.10 +declaration {* fn _ =>
    4.11 +  (* repeated from Traces.ML *)
    4.12 +  Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
    4.13  *}
    4.14  
    4.15  lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
     5.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:28:17 2008 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Mar 19 22:47:35 2008 +0100
     5.3 @@ -68,7 +68,7 @@
     5.4    "Finite (mksch A B$tr$x$y) --> Finite tr"
     5.5  
     5.6  
     5.7 -ML_setup {* change_simpset (fn ss => ss setmksym (K NONE)) *}
     5.8 +declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
     5.9  
    5.10  
    5.11  subsection "mksch rewrite rules"
    5.12 @@ -967,7 +967,7 @@
    5.13  done
    5.14  
    5.15  
    5.16 -ML_setup {* change_simpset (fn ss => ss setmksym (SOME o symmetric_fun)) *}
    5.17 +declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
    5.18  
    5.19  
    5.20  end
     6.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:28:17 2008 +0100
     6.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Wed Mar 19 22:47:35 2008 +0100
     6.3 @@ -90,7 +90,7 @@
     6.4  lemmas [simp del] = ex_simps all_simps split_paired_Ex
     6.5  declare Let_def [simp]
     6.6  
     6.7 -ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
     6.8 +declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
     6.9  
    6.10  
    6.11  subsection {* ex2seqC *}
     7.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:28:17 2008 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Mar 19 22:47:35 2008 +0100
     7.3 @@ -195,7 +195,7 @@
     7.4  
     7.5  lemmas [simp del] = ex_simps all_simps split_paired_Ex
     7.6  declare Let_def [simp]
     7.7 -ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *}
     7.8 +declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
     7.9  
    7.10  lemmas exec_rws = executions_def is_exec_frag_def
    7.11  
     8.1 --- a/src/ZF/Main_ZF.thy	Wed Mar 19 22:28:17 2008 +0100
     8.2 +++ b/src/ZF/Main_ZF.thy	Wed Mar 19 22:47:35 2008 +0100
     8.3 @@ -72,8 +72,8 @@
     8.4  by (rule transrec3_def [THEN def_transrec, THEN trans], force)
     8.5  
     8.6  
     8.7 -ML_setup {*
     8.8 -  change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
     8.9 +declaration {* fn _ =>
    8.10 +  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    8.11  *}
    8.12  
    8.13  end
     9.1 --- a/src/ZF/OrdQuant.thy	Wed Mar 19 22:28:17 2008 +0100
     9.2 +++ b/src/ZF/OrdQuant.thy	Wed Mar 19 22:47:35 2008 +0100
     9.3 @@ -362,7 +362,9 @@
     9.4      atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
     9.5                   ZF_conn_pairs,
     9.6               ZF_mem_pairs);
     9.7 -change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
     9.8 +*}
     9.9 +declaration {* fn _ =>
    9.10 +  Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
    9.11  *}
    9.12  
    9.13  text {* Setting up the one-point-rule simproc *}