# HG changeset patch
# User wenzelm
# Date 1122916898 -7200
# Node ID 7dfc99f62dd95d8756b4ea71a1a60c9fd4694ade
# Parent  32afaa947f6edabf18b359a5cfcbbc937ed10202
* Pure/Simplifier: improved handling of bound variables;

diff -r 32afaa947f6e -r 7dfc99f62dd9 NEWS
--- a/NEWS	Mon Aug 01 19:20:49 2005 +0200
+++ b/NEWS	Mon Aug 01 19:21:38 2005 +0200
@@ -582,9 +582,14 @@
 
 * Pure: print_tac now outputs the goal through the trace channel.
 
-* 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
+* Pure/Simplifier: improved handling of bound variables (nameless
+representation, avoid allocating new strings).  Simprocs that invoke
+the Simplifier recursively should use Simplifier.inherit_bounds to
+avoid local name clashes.
+
+* Pure/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: