equal
deleted
inserted
replaced
312 |
312 |
313 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
313 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
314 |
314 |
315 |
315 |
316 *** ML *** |
316 *** ML *** |
|
317 |
|
318 * Simproc programming interfaces have been simplified: |
|
319 Simplifier.make_simproc and Simplifier.define_simproc supersede various |
|
320 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
|
321 term patterns for the left-hand sides are specified with implicitly |
|
322 fixed variables, like top-level theorem statements. INCOMPATIBILITY. |
317 |
323 |
318 * Instantiation rules have been re-organized as follows: |
324 * Instantiation rules have been re-organized as follows: |
319 |
325 |
320 Thm.instantiate (*low-level instantiation with named arguments*) |
326 Thm.instantiate (*low-level instantiation with named arguments*) |
321 Thm.instantiate' (*version with positional arguments*) |
327 Thm.instantiate' (*version with positional arguments*) |