--- 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)