equal
deleted
inserted
replaced
623 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
623 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
624 remove '!' and add '?' as required. |
624 remove '!' and add '?' as required. |
625 |
625 |
626 |
626 |
627 *** ML *** |
627 *** ML *** |
|
628 |
|
629 * Isar proof methods are based on a slightly more general type |
|
630 context_tactic, which allows to change the proof context dynamically |
|
631 (e.g. to update cases) and indicate explicit Seq.Error results. Former |
|
632 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are |
|
633 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. |
628 |
634 |
629 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
635 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
630 |
636 |
631 * The auxiliary module Pure/display.ML has been eliminated. Its |
637 * The auxiliary module Pure/display.ML has been eliminated. Its |
632 elementary thm print operations are now in Pure/more_thm.ML and thus |
638 elementary thm print operations are now in Pure/more_thm.ML and thus |