1.1 --- a/NEWS	Mon Jan 02 20:50:17 2006 +0100
     1.2 +++ b/NEWS	Tue Jan 03 00:06:18 2006 +0100
     1.3 @@ -65,6 +65,11 @@
     1.4  
     1.5    def x == "t" and y == "u"
     1.6  
     1.7 +* Isar: added command 'unfolding', which is structurally similar to
     1.8 +'using', but affects both the goal state and facts by unfolding given
     1.9 +meta-level equations.  Thus many occurrences of the 'unfold' method or
    1.10 +'unfolded' attribute may be replaced by first-class proof text.
    1.11 +
    1.12  * Provers/induct: improved internal context management to support
    1.13  local fixes and defines on-the-fly.  Thus explicit meta-level
    1.14  connectives !! and ==> are rarely required anymore in inductive goals
    1.15 @@ -225,14 +230,15 @@
    1.16    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.17    val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
    1.18  
    1.19 -The semantics of "burrow" is: "take a function with *simulatanously* transforms
    1.20 -a list of value, and apply it *simulatanously* to a list of list of values of the
    1.21 -appropriate type". Confer this with "map" which would *not* apply its argument
    1.22 -function simulatanously but in sequence. "burrow_split" allows the transformator
    1.23 -function to yield an additional side result.
    1.24 -
    1.25 -Both actually avoid the usage of "unflat" since they hide away "unflat"
    1.26 -from the user.
    1.27 +The semantics of "burrow" is: "take a function with *simulatanously*
    1.28 +transforms a list of value, and apply it *simulatanously* to a list of
    1.29 +list of values of the appropriate type". Confer this with "map" which
    1.30 +would *not* apply its argument function simulatanously but in
    1.31 +sequence. "burrow_split" allows the transformator function to yield an
    1.32 +additional side result.
    1.33 +
    1.34 +Both actually avoid the usage of "unflat" since they hide away
    1.35 +"unflat" from the user.
    1.36  
    1.37  * Pure/library: functions map2 and fold2 with curried syntax for
    1.38  simultanous mapping and folding:
    1.39 @@ -256,13 +262,6 @@
    1.40  * Pure/General: name_mangler.ML provides a functor for generic name
    1.41  mangling (bijective mapping from any expression values to strings).
    1.42  
    1.43 -* Pure/library:
    1.44 -
    1.45 -  val is_prefix: ('a * 'a -> bool) -> 'a list -> 'a list -> bool
    1.46 -
    1.47 -  replacing infix "prefix" and various individual isomorphic functions scattered
    1.48 -  among an amount of ML modules.
    1.49 -
    1.50  * Pure/General: rat.ML implements rational numbers.
    1.51  
    1.52  * Pure: several functions of signature "... -> theory -> theory * ..."
    1.53 @@ -278,7 +277,7 @@
    1.54  slightly more general idea of ``protecting'' meta-level rule
    1.55  statements.
    1.56  
    1.57 -* Internal goals: structure Goal provides simple interfaces for
    1.58 +* Pure/goals: structure Goal provides simple interfaces for
    1.59  init/conclude/finish and tactical prove operations (replacing former
    1.60  Tactic.prove).  Note that OldGoals.prove_goalw_cterm has long been
    1.61  obsolete, it is ill-behaved in a local proof context (e.g. with local
    1.62 @@ -302,6 +301,9 @@
    1.63  theory; raw versions simpset/claset_ref etc. have been discontinued --
    1.64  INCOMPATIBILITY.
    1.65  
    1.66 +* Provers: more generic wrt. syntax of object-logics, avoid hardwired
    1.67 +"Trueprop" etc.
    1.68 +
    1.69  
    1.70  
    1.71  New in Isabelle2005 (October 2005)