1.1 --- a/NEWS	Thu Sep 29 15:31:34 2005 +0200
     1.2 +++ b/NEWS	Thu Sep 29 15:50:43 2005 +0200
     1.3 @@ -1,8 +1,8 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in Isabelle2005 (September 2005)
     1.8 -------------------------------------
     1.9 +New in Isabelle2005 (October 2005)
    1.10 +----------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 @@ -125,6 +125,9 @@
    1.15  * Delimiters of outer tokens (string etc.) now produce separate LaTeX
    1.16  macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
    1.17  
    1.18 +* Isabelle's pdfsetup.sty now requires ifpdf.sty (which is part of
    1.19 +common LaTeX distributions) for robust checking of PDF output mode.
    1.20 +
    1.21  * isatool usedir: new option -C (default true) controls whether option
    1.22  -D should include a copy of the original document directory; -C false
    1.23  prevents unwanted effects such as copying of administrative CVS data.
    1.24 @@ -952,32 +955,9 @@
    1.25  * Simplifier: improved handling of bound variables (nameless
    1.26  representation, avoid allocating new strings).  Simprocs that invoke
    1.27  the Simplifier recursively should use Simplifier.inherit_bounds to
    1.28 -avoid local name clashes.
    1.29 -
    1.30 -* Provers: Simplifier and Classical Reasoner now support proof context
    1.31 -dependent plug-ins (simprocs, solvers, wrappers etc.).  These extra
    1.32 -components are stored in the theory and patched into the
    1.33 -simpset/claset when used in an Isar proof context.  Context dependent
    1.34 -components are maintained by the following theory operations:
    1.35 -
    1.36 -  Simplifier.add_context_simprocs
    1.37 -  Simplifier.del_context_simprocs
    1.38 -  Simplifier.set_context_subgoaler
    1.39 -  Simplifier.reset_context_subgoaler
    1.40 -  Simplifier.add_context_looper
    1.41 -  Simplifier.del_context_looper
    1.42 -  Simplifier.add_context_unsafe_solver
    1.43 -  Simplifier.add_context_safe_solver
    1.44 -
    1.45 -  Classical.add_context_safe_wrapper
    1.46 -  Classical.del_context_safe_wrapper
    1.47 -  Classical.add_context_unsafe_wrapper
    1.48 -  Classical.del_context_unsafe_wrapper
    1.49 -
    1.50 -IMPORTANT NOTE: proof tools (methods etc.) need to use
    1.51 -local_simpset_of and local_claset_of instead of the primitive
    1.52 -Simplifier.get_local_simpset and Classical.get_local_claset,
    1.53 -respectively, in order to see the context dependent fields!
    1.54 +avoid local name clashes.  Failure to do so produces warnings
    1.55 +"Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds
    1.56 +for further details.
    1.57  
    1.58  * ML functions legacy_bindings and use_legacy_bindings produce ML fact
    1.59  bindings for all theorems stored within a given theory; this may help