105 fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, |
105 fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, |
106 lessD = lessD1, simpset = simpset1}, |
106 lessD = lessD1, simpset = simpset1}, |
107 {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, |
107 {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, |
108 lessD = lessD2, simpset = simpset2}) = |
108 lessD = lessD2, simpset = simpset2}) = |
109 {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), |
109 {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), |
110 mult_mono_thms = gen_merge_lists' (eq_thm o pairself fst) mult_mono_thms1 mult_mono_thms2, |
110 mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst) |
|
111 mult_mono_thms1 mult_mono_thms2, |
111 inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), |
112 inj_thms = Drule.merge_rules (inj_thms1, inj_thms2), |
112 lessD = Drule.merge_rules (lessD1, lessD2), |
113 lessD = Drule.merge_rules (lessD1, lessD2), |
113 simpset = Simplifier.merge_ss (simpset1, simpset2)}; |
114 simpset = Simplifier.merge_ss (simpset1, simpset2)}; |
114 |
115 |
115 fun print _ _ = (); |
116 fun print _ _ = (); |