tuned signature;
authorwenzelm
Sat Mar 31 19:26:23 2012 +0200 (2012-03-31)
changeset 472390b1829860149
parent 47238 289dcbdd5984
child 47240 72ab1fbf2f41
tuned signature;
src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
src/Pure/drule.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Mar 31 19:09:59 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Sat Mar 31 19:26:23 2012 +0200
     1.3 @@ -967,7 +967,7 @@
     1.4  done
     1.5  
     1.6  
     1.7 -declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (SOME o symmetric_fun))) *}
     1.8 +declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}
     1.9  
    1.10  
    1.11  end
     2.1 --- a/src/Pure/drule.ML	Sat Mar 31 19:09:59 2012 +0200
     2.2 +++ b/src/Pure/drule.ML	Sat Mar 31 19:26:23 2012 +0200
     2.3 @@ -43,7 +43,6 @@
     2.4    val reflexive_thm: thm
     2.5    val symmetric_thm: thm
     2.6    val transitive_thm: thm
     2.7 -  val symmetric_fun: thm -> thm
     2.8    val extensional: thm -> thm
     2.9    val asm_rl: thm
    2.10    val cut_rl: thm
    2.11 @@ -400,8 +399,6 @@
    2.12      val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
    2.13    in store_standard_thm_open (Binding.name "transitive") thm end;
    2.14  
    2.15 -fun symmetric_fun thm = thm RS symmetric_thm;
    2.16 -
    2.17  fun extensional eq =
    2.18    let val eq' =
    2.19      Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq
     3.1 --- a/src/Pure/raw_simplifier.ML	Sat Mar 31 19:09:59 2012 +0200
     3.2 +++ b/src/Pure/raw_simplifier.ML	Sat Mar 31 19:26:23 2012 +0200
     3.3 @@ -101,6 +101,7 @@
     3.4    val solver: simpset -> solver -> int -> tactic
     3.5    val simp_depth_limit_raw: Config.raw
     3.6    val clear_ss: simpset -> simpset
     3.7 +  val default_mk_sym: simpset -> thm -> thm option
     3.8    val simproc_global_i: theory -> string -> term list
     3.9      -> (theory -> simpset -> term -> thm option) -> simproc
    3.10    val simproc_global: theory -> string -> string list
    3.11 @@ -766,11 +767,13 @@
    3.12    init_ss mk_rews termless subgoal_tac solvers
    3.13    |> inherit_context ss;
    3.14  
    3.15 +fun default_mk_sym _ th = SOME (th RS Drule.symmetric_thm);
    3.16 +
    3.17  val empty_ss =
    3.18    init_ss
    3.19      {mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
    3.20        mk_cong = K I,
    3.21 -      mk_sym = K (SOME o Drule.symmetric_fun),
    3.22 +      mk_sym = default_mk_sym,
    3.23        mk_eq_True = K (K NONE),
    3.24        reorient = default_reorient}
    3.25      Term_Ord.termless (K (K no_tac)) ([], []);
     4.1 --- a/src/Pure/simplifier.ML	Sat Mar 31 19:09:59 2012 +0200
     4.2 +++ b/src/Pure/simplifier.ML	Sat Mar 31 19:26:23 2012 +0200
     4.3 @@ -33,6 +33,7 @@
     4.4    val map_simpset_global: (simpset -> simpset) -> theory -> theory
     4.5    val pretty_ss: Proof.context -> simpset -> Pretty.T
     4.6    val clear_ss: simpset -> simpset
     4.7 +  val default_mk_sym: simpset -> thm -> thm option
     4.8    val debug_bounds: bool Unsynchronized.ref
     4.9    val prems_of: simpset -> thm list
    4.10    val add_simp: thm -> simpset -> simpset