equal
deleted
inserted
replaced
325 |
325 |
326 * Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. |
326 * Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. |
327 |
327 |
328 |
328 |
329 *** ML *** |
329 *** ML *** |
|
330 |
|
331 * The auxiliary module Pure/display.ML has been eliminated. Its |
|
332 elementary thm print operations are now in Pure/more_thm.ML and thus |
|
333 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. |
330 |
334 |
331 * Simproc programming interfaces have been simplified: |
335 * Simproc programming interfaces have been simplified: |
332 Simplifier.make_simproc and Simplifier.define_simproc supersede various |
336 Simplifier.make_simproc and Simplifier.define_simproc supersede various |
333 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
337 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
334 term patterns for the left-hand sides are specified with implicitly |
338 term patterns for the left-hand sides are specified with implicitly |