1.1 --- a/NEWS	Sat Oct 15 00:08:13 2005 +0200
     1.2 +++ b/NEWS	Sat Oct 15 00:08:14 2005 +0200
     1.3 @@ -9,8 +9,23 @@
     1.4  * Command 'find_theorems': support "*" wildcard in "name:" criterion.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* Added antiquotations @{ML_type text} and @{ML_struct} which check
    1.10 +the given source text as ML type/structure, printing verbatim.
    1.11 +
    1.12 +
    1.13  *** Pure ***
    1.14  
    1.15 +* Isar: improper proof element 'guess' is like 'obtain', but derives
    1.16 +the obtained context from the course of reasoning!  For example:
    1.17 +
    1.18 +  assume "EX x y. A x & B y"   -- "any previous fact"
    1.19 +  then guess x and y by clarify
    1.20 +
    1.21 +This technique is potentially adventurous, depending on the facts and
    1.22 +proof tools being involved here.
    1.23 +
    1.24  * Input syntax now supports dummy variable binding "%_. b", where the
    1.25  body does not mention the bound variable.  Note that dummy patterns
    1.26  implicitly depend on their context of bounds, which makes "{_. _}"
    1.27 @@ -22,16 +37,18 @@
    1.28  translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
    1.29  example "A -> B" => "Pi A (%_. B)".
    1.30  
    1.31 +
    1.32  *** HOL ***
    1.33  
    1.34 -* In the context of the assumption "~(s = t)" the simplifier rewrites
    1.35 -"t = s" to False (by simproc "neq_simproc"). For backward compatibility
    1.36 -this can be disabled by ML"reset use_neq_simproc".
    1.37 +* In the context of the assumption "~(s = t)" the Simplifier rewrites
    1.38 +"t = s" to False (by simproc "neq_simproc").  For backward
    1.39 +compatibility this can be disabled by ML "reset use_neq_simproc".
    1.40  
    1.41  * Tactics 'sat' and 'satx' reimplemented, several improvements: goals
    1.42  no longer need to be stated as "<prems> ==> False", equivalences (i.e.
    1.43 -"=" on type bool) are handled, variable names of the form "lit_<n>" are
    1.44 -no longer reserved, significant speedup.
    1.45 +"=" on type bool) are handled, variable names of the form "lit_<n>"
    1.46 +are no longer reserved, significant speedup.
    1.47 +
    1.48  
    1.49  
    1.50  New in Isabelle2005 (October 2005)