# HG changeset patch
# User wenzelm
# Date 1152356066 -7200
# Node ID 02c59ec2f2e16e9c47ecb36716eb3963a142ae60
# Parent  4293f932fe83f3aa318875b5615dccbe44c1755f
* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
* Pure: Goal.prove, Goal.prove_global;
tuned;

diff -r 4293f932fe83 -r 02c59ec2f2e1 NEWS
--- a/NEWS	Fri Jul 07 18:13:58 2006 +0200
+++ b/NEWS	Sat Jul 08 12:54:26 2006 +0200
@@ -563,10 +563,6 @@
 signature declarations.  (This information is not relevant to the
 logic, but only for type inference.)  IMPORTANT INTERNAL CHANGE.
 
-* Pure: Logic.(un)varify only works in a global context, which is now
-enforced instead of silently assumed.  INCOMPATIBILITY, may use
-Logic.legacy_(un)varify as temporary workaround.
-
 * Pure: axiomatic type classes are now purely definitional, with
 explicit proofs of class axioms and super class relations performed
 internally.  See Pure/axclass.ML for the main internal interfaces --
@@ -593,11 +589,24 @@
 slightly more general idea of ``protecting'' meta-level rule
 statements.
 
+* Pure: Logic.(un)varify only works in a global context, which is now
+enforced instead of silently assumed.  INCOMPATIBILITY, may use
+Logic.legacy_(un)varify as temporary workaround.
+
+* Pure: structure Variable provides fundamental operations for proper
+treatment of fixed/schematic variables in a context.  For example,
+Variable.import introduces fixes for schematics of given facts and
+Variable.export reverses the effect (up to renaming) -- this replaces
+various freeze_thaw operations.
+
 * Pure: 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).
+Tactic.prove).  Goal.prove is the canonical way to prove results
+within a given context; Goal.prove_global is a degraded version for
+theory level goals, including a global Drule.standard.  Note that
+OldGoals.prove_goalw_cterm has long been obsolete, since it is
+ill-behaved in a local proof context (e.g. with local fixes/assumes or
+in a locale context).
 
 * Isar: simplified treatment of user-level errors, using exception
 ERROR of string uniformly.  Function error now merely raises ERROR,