1.1 --- a/NEWS Tue Sep 25 12:59:24 2007 +0200
1.2 +++ b/NEWS Tue Sep 25 13:28:35 2007 +0200
1.3 @@ -1164,12 +1164,10 @@
1.4 * ML basics: just one true type int, which coincides with IntInf.int
1.5 (even on SML/NJ).
1.6
1.7 -* Generic arithmetic modules: Tools/rat.ML, Tools/float.ML
1.8 -
1.9 * Context data interfaces (Theory/Proof/GenericDataFun): removed
1.10 name/print, uninitialized data defaults to ad-hoc copy of empty value,
1.11 -init only required for impure data. INCOMPATIBILITY: empty really
1.12 -need to be empty (no dependencies on theory content!)
1.13 +init only required for impure data. INCOMPATIBILITY: empty really need
1.14 +to be empty (no dependencies on theory content!)
1.15
1.16 * ML within Isar: antiquotations allow to embed statically-checked
1.17 formal entities in the source, referring to the context available at
1.18 @@ -1198,7 +1196,7 @@
1.19 The same works for sources being ``used'' within an Isar context.
1.20
1.21 * ML in Isar: improved error reporting; extra verbosity with
1.22 -Toplevel.debug enabled.
1.23 +ML_Context.trace enabled.
1.24
1.25 * Pure/library:
1.26
1.27 @@ -1211,12 +1209,6 @@
1.28 would *not* apply its argument function simulatanously but in
1.29 sequence; "fold_burrow" has an additional context.
1.30
1.31 -* Pure/library: functions map2 and fold2 with curried syntax for
1.32 -simultanous mapping and folding:
1.33 -
1.34 - val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
1.35 - val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
1.36 -
1.37 * Pure/library: indexed lists - some functions in the Isabelle library
1.38 treating lists over 'a as finite mappings from [0...n] to 'a have been
1.39 given more convenient names and signatures reminiscent of similar
1.40 @@ -1229,11 +1221,8 @@
1.41 Note that fold_index starts counting at index 0, not 1 like foldln
1.42 used to.
1.43
1.44 -* Pure/library: added general ``divide_and_conquer'' combinator on
1.45 -lists.
1.46 -
1.47 * Pure/General/table.ML: the join operations now works via exceptions
1.48 -DUP/SAME instead of type option. This is simpler in simple cases, and
1.49 +DUP/SAME instead of type option. This is simpler in simple cases, and
1.50 admits slightly more efficient complex applications.
1.51
1.52 * Pure: datatype Context.generic joins theory/Proof.context and
1.53 @@ -1244,24 +1233,24 @@
1.54 use Context.generic instead of just theory.
1.55
1.56 * Pure: simplified internal attribute type, which is now always
1.57 -Context.generic * thm -> Context.generic * thm. Global (theory)
1.58 -vs. local (Proof.context) attributes have been discontinued, while
1.59 -minimizing code duplication. Thm.rule_attribute and
1.60 -Thm.declaration_attribute build canonical attributes; see also
1.61 -structure Context for further operations on Context.generic, notably
1.62 -GenericDataFun. INCOMPATIBILITY, need to adapt attribute type
1.63 +Context.generic * thm -> Context.generic * thm. Global (theory) vs.
1.64 +local (Proof.context) attributes have been discontinued, while
1.65 +minimizing code duplication. Thm.rule_attribute and
1.66 +Thm.declaration_attribute build canonical attributes; see also structure
1.67 +Context for further operations on Context.generic, notably
1.68 +GenericDataFun. INCOMPATIBILITY, need to adapt attribute type
1.69 declarations and definitions.
1.70
1.71 * Pure/kernel: consts certification ignores sort constraints given in
1.72 -signature declarations. (This information is not relevant to the
1.73 -logic, but only for type inference.) IMPORTANT INTERNAL CHANGE,
1.74 -potential INCOMPATIBILITY.
1.75 +signature declarations. (This information is not relevant to the logic,
1.76 +but only for type inference.) IMPORTANT INTERNAL CHANGE, potential
1.77 +INCOMPATIBILITY.
1.78
1.79 * Pure: axiomatic type classes are now purely definitional, with
1.80 explicit proofs of class axioms and super class relations performed
1.81 -internally. See Pure/axclass.ML for the main internal interfaces --
1.82 +internally. See Pure/axclass.ML for the main internal interfaces --
1.83 notably AxClass.define_class supercedes AxClass.add_axclass, and
1.84 -AxClass.axiomatize_class/classrel/arity supercede
1.85 +AxClass.axiomatize_class/classrel/arity supersede
1.86 Sign.add_classes/classrel/arities.
1.87
1.88 * Pure/Isar: Args/Attrib parsers operate on Context.generic --
1.89 @@ -1318,6 +1307,11 @@
1.90 ill-behaved in a local proof context (e.g. with local fixes/assumes or
1.91 in a locale context).
1.92
1.93 +* Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.)
1.94 +and type checking (Syntax.check_term etc.), with common combinations
1.95 +(Syntax.read_term etc.). These supersede former Sign.read_term etc.
1.96 +which are considered legacy and await removal.
1.97 +
1.98 * Isar: simplified treatment of user-level errors, using exception
1.99 ERROR of string uniformly. Function error now merely raises ERROR,
1.100 without any side effect on output channels. The Isar toplevel takes
1.101 @@ -1340,8 +1334,8 @@
1.102 * Isar: theory setup now has type (theory -> theory), instead of a
1.103 list. INCOMPATIBILITY, may use #> to compose setup functions.
1.104
1.105 -* Isar: installed ML toplevel pretty printer for type Proof.context,
1.106 -subject to ProofContext.debug/verbose flags.
1.107 +* Isar: ML toplevel pretty printer for type Proof.context, subject to
1.108 +ProofContext.debug/verbose flags.
1.109
1.110 * Isar: Toplevel.theory_to_proof admits transactions that modify the
1.111 theory before entering a proof state. Transactions now always see a