equal
deleted
inserted
replaced
140 |
140 |
141 local |
141 local |
142 val remove_trigger = @{lemma "trigger t p == p" |
142 val remove_trigger = @{lemma "trigger t p == p" |
143 by (rule eq_reflection, rule trigger_def)} |
143 by (rule eq_reflection, rule trigger_def)} |
144 |
144 |
145 val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true] |
145 val remove_weight = @{lemma "weight w p == p" |
|
146 by (rule eq_reflection, rule weight_def)} |
|
147 |
|
148 val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight, |
|
149 L.rewrite_true] |
146 |
150 |
147 fun rewrite_conv ctxt eqs = Simplifier.full_rewrite |
151 fun rewrite_conv ctxt eqs = Simplifier.full_rewrite |
148 (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) |
152 (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs) |
149 |
153 |
150 fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs))) |
154 fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs))) |