# HG changeset patch
# User wenzelm
# Date 1089570865 -7200
# Node ID 255bc508a7569a0d9709ff957fa0a667a5a28909
# Parent  02aed07e01bf323406f58dd7a05090e242638cb0
Simplifier and Classical Reasoner now support proof context dependent plug-ins;

diff -r 02aed07e01bf -r 255bc508a756 NEWS
--- a/NEWS	Sun Jul 11 20:33:22 2004 +0200
+++ b/NEWS	Sun Jul 11 20:34:25 2004 +0200
@@ -44,6 +44,9 @@
   yet). If false the first entry wins (as during parsing). Default
   value is true.
 
+* Pure: tuned internal renaming of symbolic identifiers -- attach
+  primes instead of base 26 numbers.
+
 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,
@@ -53,8 +56,39 @@
   etc.) may depend on the signature of the theory context being
   presently used for parsing/printing, see also isar-ref manual.
 
-* Pure: tuned internal renaming of symbolic identifiers -- attach
-  primes instead of base 26 numbers.
+* Pure/Simplifier: simplification procedures may now take the current
+  simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
+  interface), which is very useful for calling the Simplifier
+  recursively.  Minor INCOMPATIBILITY: the 'prems' argument of
+  simprocs is gone -- use prems_of_ss on the simpset instead.
+  Moreover, the low-level mk_simproc no longer applies Logic.varify
+  internally, to allow for use in a context of fixed variables.
+
+* Provers: Simplifier and Classical Reasoner now support proof context
+  dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
+  components are stored in the theory and patched into the
+  simpset/claset when used in an Isar proof context.  Context
+  dependent components are maintained by the following theory
+  operations:
+
+    Simplifier.add_context_simprocs
+    Simplifier.del_context_simprocs
+    Simplifier.set_context_subgoaler
+    Simplifier.reset_context_subgoaler
+    Simplifier.add_context_looper
+    Simplifier.del_context_looper
+    Simplifier.add_context_unsafe_solver
+    Simplifier.add_context_safe_solver
+
+    Classical.add_context_safe_wrapper
+    Classical.del_context_safe_wrapper
+    Classical.add_context_unsafe_wrapper
+    Classical.del_context_unsafe_wrapper
+
+  IMPORTANT NOTE: proof tools (methods etc.) need to use
+  local_simpset_of and local_claset_of to instead of the primitive
+  Simplifier.get_local_simpset and Classical.get_local_claset,
+  respectively, in order to see the context dependent fields!
 
 * Document preparation: antiquotations now provide the option
   'locale=NAME' to specify an alternative context used for evaluating
@@ -69,14 +103,6 @@
   these are subject to the DVI_VIEWER and PRINT_COMMAND settings,
   respectively.
 
-* ML: simplification procedures may now take the current simpset into
-  account (cf. Simplifier.simproc(_i) / mk_simproc interface), which
-  is very useful for calling the Simplifier recursively.  Minor
-  INCOMPATIBILITY: the 'prems' argument of simprocs is gone -- use
-  prems_of_ss on the simpset instead.  Moreover, the low-level
-  mk_simproc no longer applies Logic.varify internally, to allow for
-  use in a context of fixed variables.
-
 * ML: output via the Isabelle channels of writeln/warning/error
   etc. is now passed through Output.output, with a hook for arbitrary
   transformations depending on the print_mode (cf. Output.add_mode --