equal
deleted
inserted
replaced
465 |
465 |
466 fun norm_term thy t = |
466 fun norm_term thy t = |
467 let |
467 let |
468 val norms = ShuffleData.get thy |
468 val norms = ShuffleData.get thy |
469 val ss = Simplifier.global_context thy empty_ss |
469 val ss = Simplifier.global_context thy empty_ss |
470 setmksimps (K single) |
|
471 addsimps (map (Thm.transfer thy) norms) |
470 addsimps (map (Thm.transfer thy) norms) |
472 addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] |
471 addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy] |
473 fun chain f th = |
472 fun chain f th = |
474 let |
473 let |
475 val rhs = Thm.rhs_of th |
474 val rhs = Thm.rhs_of th |