equal
deleted
inserted
replaced
1103 |
1103 |
1104 fun rewrite_eqn conv ctxt = |
1104 fun rewrite_eqn conv ctxt = |
1105 singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt) |
1105 singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt) |
1106 |
1106 |
1107 fun preprocess conv ctxt = |
1107 fun preprocess conv ctxt = |
1108 Thm.transfer (Proof_Context.theory_of ctxt) |
1108 Thm.transfer' ctxt |
1109 #> rewrite_eqn conv ctxt |
1109 #> rewrite_eqn conv ctxt |
1110 #> Axclass.unoverload ctxt; |
1110 #> Axclass.unoverload ctxt; |
1111 |
1111 |
1112 fun cert_of_eqns_preprocess ctxt functrans c = |
1112 fun cert_of_eqns_preprocess ctxt functrans c = |
1113 let |
1113 let |