# HG changeset patch
# User wenzelm
# Date 1129327694 -7200
# Node ID 5b0c3dcfbad22be0275b7b151717ee39ca0aab64
# Parent  b039ea8bb9656a272c959109dbf54a5d37dded61
* antiquotations ML_type, ML_struct;
* Isar 'guess' element;

diff -r b039ea8bb965 -r 5b0c3dcfbad2 NEWS
--- a/NEWS	Sat Oct 15 00:08:13 2005 +0200
+++ b/NEWS	Sat Oct 15 00:08:14 2005 +0200
@@ -9,8 +9,23 @@
 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
 
 
+*** Document preparation ***
+
+* Added antiquotations @{ML_type text} and @{ML_struct} which check
+the given source text as ML type/structure, printing verbatim.
+
+
 *** Pure ***
 
+* Isar: improper proof element 'guess' is like 'obtain', but derives
+the obtained context from the course of reasoning!  For example:
+
+  assume "EX x y. A x & B y"   -- "any previous fact"
+  then guess x and y by clarify
+
+This technique is potentially adventurous, depending on the facts and
+proof tools being involved here.
+
 * Input syntax now supports dummy variable binding "%_. b", where the
 body does not mention the bound variable.  Note that dummy patterns
 implicitly depend on their context of bounds, which makes "{_. _}"
@@ -22,16 +37,18 @@
 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
 example "A -> B" => "Pi A (%_. B)".
 
+
 *** HOL ***
 
-* In the context of the assumption "~(s = t)" the simplifier rewrites
-"t = s" to False (by simproc "neq_simproc"). For backward compatibility
-this can be disabled by ML"reset use_neq_simproc".
+* In the context of the assumption "~(s = t)" the Simplifier rewrites
+"t = s" to False (by simproc "neq_simproc").  For backward
+compatibility this can be disabled by ML "reset use_neq_simproc".
 
 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals
 no longer need to be stated as "<prems> ==> False", equivalences (i.e.
-"=" on type bool) are handled, variable names of the form "lit_<n>" are
-no longer reserved, significant speedup.
+"=" on type bool) are handled, variable names of the form "lit_<n>"
+are no longer reserved, significant speedup.
+
 
 
 New in Isabelle2005 (October 2005)