equal
deleted
inserted
replaced
1334 |
1334 |
1335 * Isar: Toplevel.theory_to_proof admits transactions that modify the |
1335 * Isar: Toplevel.theory_to_proof admits transactions that modify the |
1336 theory before entering a proof state. Transactions now always see a |
1336 theory before entering a proof state. Transactions now always see a |
1337 quasi-functional intermediate checkpoint, both in interactive and |
1337 quasi-functional intermediate checkpoint, both in interactive and |
1338 batch mode. |
1338 batch mode. |
|
1339 |
|
1340 * Isar: simplified interfaces for outer syntax. Renamed |
|
1341 OuterSyntax.add_keywords to OuterSyntax.keywords. Removed |
|
1342 OuterSyntax.add_parsers -- this functionality is now included in |
|
1343 OuterSyntax.command etc. INCOMPATIBILITY. |
1339 |
1344 |
1340 * Simplifier: the simpset of a running simplification process now |
1345 * Simplifier: the simpset of a running simplification process now |
1341 contains a proof context (cf. Simplifier.the_context), which is the |
1346 contains a proof context (cf. Simplifier.the_context), which is the |
1342 very context that the initial simpset has been retrieved from (by |
1347 very context that the initial simpset has been retrieved from (by |
1343 simpset_of/local_simpset_of). Consequently, all plug-in components |
1348 simpset_of/local_simpset_of). Consequently, all plug-in components |