# HG changeset patch
# User wenzelm
# Date 1129583416 -7200
# Node ID 5b9efe4d6b47ec51f1b2e327b31c1a4231aa7d67
# Parent  67d5ab1cb0d8c7f75589082aa0951f216909e9c7
tuned;

diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 NEWS
--- 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)
 ----------------------------------
diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 src/LCF/ex/Ex1.ML
--- 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];
 
diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 src/LCF/ex/Ex2.ML
--- 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];
 
diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 src/LCF/ex/Ex3.ML
--- 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];
 
diff -r 67d5ab1cb0d8 -r 5b9efe4d6b47 src/LCF/ex/Ex4.ML
--- 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);