1.1 --- a/NEWS Fri Aug 23 00:12:20 2013 +0200
1.2 +++ b/NEWS Fri Aug 23 11:23:26 2013 +0200
1.3 @@ -108,8 +108,8 @@
1.4
1.5 * Target-sensitive commands 'interpretation' and 'sublocale'.
1.6 Particulary, 'interpretation' now allows for non-persistent
1.7 -interpretation within "context ... begin ... end" blocks.
1.8 -See "isar-ref" manual for details.
1.9 +interpretation within "context ... begin ... end" blocks. See
1.10 +"isar-ref" manual for details.
1.11
1.12 * Improved locales diagnostic command 'print_dependencies'.
1.13
1.14 @@ -130,39 +130,44 @@
1.15 * Improved support for adhoc overloading of constants (see also
1.16 isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
1.17
1.18 -* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly.
1.19 -Use explicit 'code equation' and 'code abstract' to distinguish both when desired.
1.20 +* Attibute 'code': 'code' now declares concrete and abstract code
1.21 +equations uniformly. Use explicit 'code equation' and 'code abstract'
1.22 +to distinguish both when desired.
1.23
1.24 * Code generator:
1.25 - * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
1.26 - * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
1.27 - subsuming 'code_modulename'.
1.28 - See the Isar reference manual for syntax diagrams, and the HOL theories for examples.
1.29 + - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
1.30 + 'code_instance'.
1.31 + - 'code_identifier' declares name hints for arbitrary identifiers in
1.32 + generated code, subsuming 'code_modulename'.
1.33 + See the isar-ref manual for syntax diagrams, and the HOL theories
1.34 + for examples.
1.35
1.36 * Library/Polynomial.thy:
1.37 - * Use lifting for primitive definitions.
1.38 - * Explicit conversions from and to lists of coefficients, used for generated code.
1.39 - * Replaced recursion operator poly_rec by fold_coeffs.
1.40 - * Prefer pre-existing gcd operation for gcd.
1.41 - * Fact renames:
1.42 + - Use lifting for primitive definitions.
1.43 + - Explicit conversions from and to lists of coefficients, used for
1.44 + generated code.
1.45 + - Replaced recursion operator poly_rec by fold_coeffs.
1.46 + - Prefer pre-existing gcd operation for gcd.
1.47 + - Fact renames:
1.48 poly_eq_iff ~> poly_eq_poly_eq_iff
1.49 poly_ext ~> poly_eqI
1.50 expand_poly_eq ~> poly_eq_iff
1.51 IMCOMPATIBILTIY.
1.52
1.53 * Reification and reflection:
1.54 - * Reification is now directly available in HOL-Main in structure "Reification".
1.55 - * Reflection now handles multiple lists with variables also.
1.56 - * The whole reflection stack has been decomposed into conversions.
1.57 + - Reification is now directly available in HOL-Main in structure
1.58 + "Reification".
1.59 + - Reflection now handles multiple lists with variables also.
1.60 + - The whole reflection stack has been decomposed into conversions.
1.61 INCOMPATIBILITY.
1.62
1.63 * Weaker precendence of syntax for big intersection and union on sets,
1.64 in accordance with corresponding lattice operations. INCOMPATIBILITY.
1.65
1.66 -* Nested case expressions are now translated in a separate check
1.67 - phase rather than during parsing. The data for case combinators
1.68 - is separated from the datatype package. The declaration attribute
1.69 - "case_translation" can be used to register new case combinators:
1.70 +* Nested case expressions are now translated in a separate check phase
1.71 +rather than during parsing. The data for case combinators is separated
1.72 +from the datatype package. The declaration attribute
1.73 +"case_translation" can be used to register new case combinators:
1.74
1.75 declare [[case_translation case_combinator constructor1 ... constructorN]]
1.76
1.77 @@ -187,7 +192,6 @@
1.78 - Fact renames:
1.79 card.union_inter ~> card_Un_Int [symmetric]
1.80 card.union_disjoint ~> card_Un_disjoint
1.81 -
1.82 INCOMPATIBILITY.
1.83
1.84 * Locale hierarchy for abstract orderings and (semi)lattices.
1.85 @@ -198,37 +202,38 @@
1.86 * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
1.87 Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.
1.88
1.89 -* Numeric types mapped by default to target language numerals:
1.90 -natural (replaces former code_numeral) and integer (replaces
1.91 -former code_int). Conversions are available as integer_of_natural /
1.92 -natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
1.93 -Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML).
1.94 -INCOMPATIBILITY.
1.95 +* Numeric types mapped by default to target language numerals: natural
1.96 +(replaces former code_numeral) and integer (replaces former code_int).
1.97 +Conversions are available as integer_of_natural / natural_of_integer /
1.98 +integer_of_nat / nat_of_integer (in HOL) and
1.99 +Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
1.100 +ML). INCOMPATIBILITY.
1.101
1.102 * Discontinued theories Code_Integer and Efficient_Nat by a more
1.103 fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
1.104 -Code_Target_Nat and Code_Target_Numeral. See the tutorial on
1.105 -code generation for details. INCOMPATIBILITY.
1.106 -
1.107 -* Introduce type class "conditionally_complete_lattice": Like a complete
1.108 - lattice but does not assume the existence of the top and bottom elements.
1.109 - Allows to generalize some lemmas about reals and extended reals.
1.110 - Removed SupInf and replaced it by the instantiation of
1.111 - conditionally_complete_lattice for real. Renamed lemmas about
1.112 - conditionally-complete lattice from Sup_... to cSup_... and from Inf_...
1.113 - to cInf_... to avoid hidding of similar complete lattice lemmas.
1.114 -
1.115 - Introduce type class linear_continuum as combination of conditionally-complete
1.116 - lattices and inner dense linorders which have more than one element.
1.117 -INCOMPATIBILITY.
1.118 -
1.119 -* Introduce type classes "no_top" and "no_bot" for orderings without top
1.120 - and bottom elements.
1.121 +Code_Target_Nat and Code_Target_Numeral. See the tutorial on code
1.122 +generation for details. INCOMPATIBILITY.
1.123 +
1.124 +* Introduce type class "conditionally_complete_lattice": Like a
1.125 +complete lattice but does not assume the existence of the top and
1.126 +bottom elements. Allows to generalize some lemmas about reals and
1.127 +extended reals. Removed SupInf and replaced it by the instantiation
1.128 +of conditionally_complete_lattice for real. Renamed lemmas about
1.129 +conditionally-complete lattice from Sup_... to cSup_... and from
1.130 +Inf_... to cInf_... to avoid hidding of similar complete lattice
1.131 +lemmas.
1.132 +
1.133 +* Introduce type class linear_continuum as combination of
1.134 +conditionally-complete lattices and inner dense linorders which have
1.135 +more than one element. INCOMPATIBILITY.
1.136 +
1.137 +* Introduce type classes "no_top" and "no_bot" for orderings without
1.138 +top and bottom elements.
1.139
1.140 * Split dense_linorder into inner_dense_order and no_top, no_bot.
1.141
1.142 * Complex_Main: Unify and move various concepts from
1.143 - HOL-Multivariate_Analysis to HOL-Complex_Main.
1.144 +HOL-Multivariate_Analysis to HOL-Complex_Main.
1.145
1.146 - Introduce type class (lin)order_topology and linear_continuum_topology.
1.147 Allows to generalize theorems about limits and order.
1.148 @@ -312,17 +317,14 @@
1.149 "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
1.150 src/HOL/Spec_Check/Examples.thy.
1.151
1.152 -* Imperative HOL: The MREC combinator is considered legacy and no longer
1.153 -included by default. INCOMPATIBILITY, use partial_function instead, or import
1.154 -theory Legacy_Mrec as a fallback.
1.155 -
1.156 -
1.157 -*** HOL-Algebra ***
1.158 -
1.159 -* Discontinued theories src/HOL/Algebra/abstract and .../poly.
1.160 -Existing theories should be based on src/HOL/Library/Polynomial
1.161 -instead. The latter provides integration with HOL's type classes for
1.162 -rings. INCOMPATIBILITY.
1.163 +* Imperative-HOL: The MREC combinator is considered legacy and no
1.164 +longer included by default. INCOMPATIBILITY, use partial_function
1.165 +instead, or import theory Legacy_Mrec as a fallback.
1.166 +
1.167 +* HOL-Algebra: Discontinued theories src/HOL/Algebra/abstract and
1.168 +.../poly. Existing theories should be based on
1.169 +src/HOL/Library/Polynomial instead. The latter provides integration
1.170 +with HOL's type classes for rings. INCOMPATIBILITY.
1.171
1.172
1.173 *** ML ***