# HG changeset patch # User wenzelm # Date 1129911417 -7200 # Node ID 2602be0d99aeadde1a3d4d3ebed13fc2099ad314 # Parent 788836292b1a684e6b1d10ce8dbbc0f1c5a9716b * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. * Internal goals: structure Goal. diff -r 788836292b1a -r 2602be0d99ae NEWS --- a/NEWS Fri Oct 21 18:15:00 2005 +0200 +++ b/NEWS Fri Oct 21 18:16:57 2005 +0200 @@ -15,9 +15,13 @@ with Isar theories; migration is usually quite simple with the ML function use_legacy_bindings. INCOMPATIBILITY. -* Legacy goal package: removed former user-level functions top_sg, -prin, printyp, pprint_term/typ, which tend to cause confusion about -the actual goal (!) context being used here. +* Legacy goal package: reduced interface to the bare minimum required +to keep existing proof scripts running. Most other user-level +functions are now part of the OldGoals structure, which is *not* open +by default (consider isatool expandshort before open OldGoals). +Removed top_sg, prin, printyp, pprint_term/typ altogether, because +these tend to cause confusion about the actual goal (!) context being +used here, which is not necessarily the same as the_context(). * Command 'find_theorems': support "*" wildcard in "name:" criterion. @@ -65,6 +69,12 @@ *** ML *** +* Internal goals: structure Goal provides simple interfaces for +init/conclude/finish and tactical prove operations (replacing former +Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been +obsolete, it is ill-behaved in a local proof context (e.g. with local +fixes/assumes or in a locale context). + * Simplifier: the simpset of a running simplification process now contains a proof context (cf. Simplifier.the_context), which is the very context that the initial simpset has been retrieved from (by