equal
deleted
inserted
replaced
185 |
185 |
186 | rew' _ = NONE; |
186 | rew' _ = NONE; |
187 in rew' end; |
187 in rew' end; |
188 |
188 |
189 fun rprocs b = [("Pure/meta_equality", rew b)]; |
189 fun rprocs b = [("Pure/meta_equality", rew b)]; |
190 val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false)); |
190 val _ = Context.>> (fold Proofterm.add_prf_rproc (rprocs false)); |
191 |
191 |
192 |
192 |
193 (**** apply rewriting function to all terms in proof ****) |
193 (**** apply rewriting function to all terms in proof ****) |
194 |
194 |
195 fun rewrite_terms r = |
195 fun rewrite_terms r = |