277 |
277 |
278 * Pure: the "Goal" constant is now called "prop", supporting a |
278 * Pure: the "Goal" constant is now called "prop", supporting a |
279 slightly more general idea of ``protecting'' meta-level rule |
279 slightly more general idea of ``protecting'' meta-level rule |
280 statements. |
280 statements. |
281 |
281 |
282 * Pure/goals: structure Goal provides simple interfaces for |
282 * Pure: structure Goal provides simple interfaces for |
283 init/conclude/finish and tactical prove operations (replacing former |
283 init/conclude/finish and tactical prove operations (replacing former |
284 Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been |
284 Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been |
285 obsolete, it is ill-behaved in a local proof context (e.g. with local |
285 obsolete, it is ill-behaved in a local proof context (e.g. with local |
286 fixes/assumes or in a locale context). |
286 fixes/assumes or in a locale context). |
|
287 |
|
288 * Pure/Isar: Toplevel.theory_theory_to_proof admits transactions that |
|
289 modify the theory before entering a proof state, i.e. the composition |
|
290 of Toplevel.theory and Toplevel.theory_to_proof. |
287 |
291 |
288 * Simplifier: the simpset of a running simplification process now |
292 * Simplifier: the simpset of a running simplification process now |
289 contains a proof context (cf. Simplifier.the_context), which is the |
293 contains a proof context (cf. Simplifier.the_context), which is the |
290 very context that the initial simpset has been retrieved from (by |
294 very context that the initial simpset has been retrieved from (by |
291 simpset_of/local_simpset_of). Consequently, all plug-in components |
295 simpset_of/local_simpset_of). Consequently, all plug-in components |