equal
deleted
inserted
replaced
98 lessD: thm list, simpset: Simplifier.simpset}; |
98 lessD: thm list, simpset: Simplifier.simpset}; |
99 |
99 |
100 val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], |
100 val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], |
101 lessD = [], simpset = Simplifier.empty_ss}; |
101 lessD = [], simpset = Simplifier.empty_ss}; |
102 val copy = I; |
102 val copy = I; |
103 val finish = I; |
|
104 val prep_ext = I; |
103 val prep_ext = I; |
105 |
104 |
106 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, |
107 lessD = lessD1, simpset = simpset1}, |
106 lessD = lessD1, simpset = simpset1}, |
108 {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, |