--- a/NEWS Mon Oct 17 23:10:15 2005 +0200
+++ b/NEWS Mon Oct 17 23:10:16 2005 +0200
@@ -50,6 +50,26 @@
are no longer reserved, significant speedup.
+*** ML ***
+
+* 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
+simpset_of/local_simpset_of). Consequently, all plug-in components
+(solver, looper etc.) may depend on arbitrary proof data.
+
+* Simplifier.inherit_context inherits the proof context (plus the
+local bounds) of the current simplification process; any simproc
+etc. that calls the Simplifier recursively should do this! Removed
+former Simplifier.inherit_bounds, which is already included here --
+INCOMPATIBILITY.
+
+* Simplifier/Classical Reasoner: more abstract interfaces
+change_simpset/claset for modifying the simpset/claset reference of a
+theory; raw versions simpset/claset_ref etc. have been discontinued --
+INCOMPATIBILITY.
+
+
New in Isabelle2005 (October 2005)
----------------------------------
--- a/src/LCF/ex/Ex1.ML Mon Oct 17 23:10:15 2005 +0200
+++ b/src/LCF/ex/Ex1.ML Mon Oct 17 23:10:16 2005 +0200
@@ -1,5 +1,5 @@
-simpset_ref() := LCF_ss;
+(* $Id$ *)
Addsimps [P_strict,K];
--- a/src/LCF/ex/Ex2.ML Mon Oct 17 23:10:15 2005 +0200
+++ b/src/LCF/ex/Ex2.ML Mon Oct 17 23:10:16 2005 +0200
@@ -1,5 +1,5 @@
-simpset_ref() := LCF_ss;
+(* $Id$ *)
Addsimps [F_strict,K];
--- a/src/LCF/ex/Ex3.ML Mon Oct 17 23:10:15 2005 +0200
+++ b/src/LCF/ex/Ex3.ML Mon Oct 17 23:10:16 2005 +0200
@@ -1,5 +1,5 @@
-simpset_ref() := LCF_ss;
+(* $Id$ *)
Addsimps [p_strict,p_s];
--- a/src/LCF/ex/Ex4.ML Mon Oct 17 23:10:15 2005 +0200
+++ b/src/LCF/ex/Ex4.ML Mon Oct 17 23:10:16 2005 +0200
@@ -1,3 +1,5 @@
+
+(* $Id$ *)
val asms = goal (the_context ()) "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
by (rewtac eq_def);