# HG changeset patch
# User wenzelm
# Date 1136243178 -3600
# Node ID 7b6f57406b1b1e446030bc367ca46858b2def1be
# Parent  35b9ed76b59ad2654ac88bd6467b710eec2977f5
* Pure/Isar: new command 'unfolding';
* ML/Provers: more generic wrt. syntax of object-logics;
tuned;

diff -r 35b9ed76b59a -r 7b6f57406b1b NEWS
--- a/NEWS	Mon Jan 02 20:50:17 2006 +0100
+++ b/NEWS	Tue Jan 03 00:06:18 2006 +0100
@@ -65,6 +65,11 @@
 
   def x == "t" and y == "u"
 
+* Isar: added command 'unfolding', which is structurally similar to
+'using', but affects both the goal state and facts by unfolding given
+meta-level equations.  Thus many occurrences of the 'unfold' method or
+'unfolded' attribute may be replaced by first-class proof text.
+
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level
 connectives !! and ==> are rarely required anymore in inductive goals
@@ -225,14 +230,15 @@
   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
 
-The semantics of "burrow" is: "take a function with *simulatanously* transforms
-a list of value, and apply it *simulatanously* to a list of list of values of the
-appropriate type". Confer this with "map" which would *not* apply its argument
-function simulatanously but in sequence. "burrow_split" allows the transformator
-function to yield an additional side result.
-
-Both actually avoid the usage of "unflat" since they hide away "unflat"
-from the user.
+The semantics of "burrow" is: "take a function with *simulatanously*
+transforms a list of value, and apply it *simulatanously* to a list of
+list of values of the appropriate type". Confer this with "map" which
+would *not* apply its argument function simulatanously but in
+sequence. "burrow_split" allows the transformator function to yield an
+additional side result.
+
+Both actually avoid the usage of "unflat" since they hide away
+"unflat" from the user.
 
 * Pure/library: functions map2 and fold2 with curried syntax for
 simultanous mapping and folding:
@@ -256,13 +262,6 @@
 * Pure/General: name_mangler.ML provides a functor for generic name
 mangling (bijective mapping from any expression values to strings).
 
-* Pure/library:
-
-  val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
-
-  replacing infix "prefix" and various individual isomorphic functions scattered
-  among an amount of ML modules.
-
 * Pure/General: rat.ML implements rational numbers.
 
 * Pure: several functions of signature "... -> theory -> theory * ..."
@@ -278,7 +277,7 @@
 slightly more general idea of ``protecting'' meta-level rule
 statements.
 
-* Internal goals: structure Goal provides simple interfaces for
+* Pure/goals: structure Goal provides simple interfaces for
 init/conclude/finish and tactical prove operations (replacing former
 Tactic.prove).  Note that OldGoals.prove_goalw_cterm has long been
 obsolete, it is ill-behaved in a local proof context (e.g. with local
@@ -302,6 +301,9 @@
 theory; raw versions simpset/claset_ref etc. have been discontinued --
 INCOMPATIBILITY.
 
+* Provers: more generic wrt. syntax of object-logics, avoid hardwired
+"Trueprop" etc.
+
 
 
 New in Isabelle2005 (October 2005)