equal
deleted
inserted
replaced
308 (** combined general normalizations **) |
308 (** combined general normalizations **) |
309 |
309 |
310 fun gen_normalize1_conv ctxt weight = |
310 fun gen_normalize1_conv ctxt weight = |
311 atomize_conv ctxt then_conv |
311 atomize_conv ctxt then_conv |
312 unfold_special_quants_conv ctxt then_conv |
312 unfold_special_quants_conv ctxt then_conv |
|
313 Thm.beta_conversion true then_conv |
313 trigger_conv ctxt then_conv |
314 trigger_conv ctxt then_conv |
314 weight_conv weight ctxt |
315 weight_conv weight ctxt |
315 |
316 |
316 fun gen_normalize1 ctxt weight thm = |
317 fun gen_normalize1 ctxt weight thm = |
317 thm |
318 thm |