--- a/NEWS Sun Sep 29 12:49:47 2013 +0200
+++ b/NEWS Sun Sep 29 12:56:50 2013 +0200
@@ -148,8 +148,9 @@
'code_instance'.
- 'code_identifier' declares name hints for arbitrary identifiers in
generated code, subsuming 'code_modulename'.
- See the isar-ref manual for syntax diagrams, and the HOL theories
- for examples.
+
+See the isar-ref manual for syntax diagrams, and the HOL theories for
+examples.
* HOL/BNF:
- Various improvements to BNF-based (co)datatype package, including new
@@ -177,9 +178,9 @@
automatically generated, which eliminate equalities of the form "f x =
t".
-* New command "fun_cases" derives ad-hoc elimination rules for
+* New command 'fun_cases' derives ad-hoc elimination rules for
function equations as simplified instances of f.elims, analogous to
-inductive_cases. See HOL/ex/Fundefs.thy for some examples.
+inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples.
* Library/Polynomial.thy:
- Use lifting for primitive definitions.
@@ -200,8 +201,9 @@
- The whole reflection stack has been decomposed into conversions.
INCOMPATIBILITY.
-* Stronger precedence of syntax for big intersection and union on sets,
-in accordance with corresponding lattice operations. INCOMPATIBILITY.
+* Stronger precedence of syntax for big intersection and union on
+sets, in accordance with corresponding lattice operations.
+INCOMPATIBILITY.
* Nested case expressions are now translated in a separate check phase
rather than during parsing. The data for case combinators is separated
@@ -230,7 +232,7 @@
semilattice_set.F correspond to former combinators fold_image
and fold1 respectively. These are now gone. You may use
those foundational constants as substitutes, but it is
- preferable to interpret the above locales accordingly.
+ preferable to interpret the above locales accordingly.
- Dropped class ab_semigroup_idem_mult (special case of lattice,
no longer needed in connection with Finite_Set.fold etc.)
- Fact renames:
@@ -242,9 +244,6 @@
* Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY.
-* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
-Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.
-
* Numeric types mapped by default to target language numerals: natural
(replaces former code_numeral) and integer (replaces former code_int).
Conversions are available as integer_of_natural / natural_of_integer /
@@ -275,9 +274,9 @@
conditionally-complete lattices and inner dense linorders which have
more than one element. INCOMPATIBILITY.
-* Introduced type classes order_top and order_bot. The old classes top
-and bot only contain the syntax without assumptions.
-INCOMPATIBILITY: Rename bot -> order_bot, top -> order_top
+* Introduced type classes order_top and order_bot. The old classes top
+and bot only contain the syntax without assumptions. INCOMPATIBILITY:
+Rename bot -> order_bot, top -> order_top
* Introduce type classes "no_top" and "no_bot" for orderings without
top and bottom elements.
@@ -287,34 +286,36 @@
* Complex_Main: Unify and move various concepts from
HOL-Multivariate_Analysis to HOL-Complex_Main.
- - Introduce type class (lin)order_topology and linear_continuum_topology.
- Allows to generalize theorems about limits and order.
- Instances are reals and extended reals.
+ - Introduce type class (lin)order_topology and
+ linear_continuum_topology. Allows to generalize theorems about
+ limits and order. Instances are reals and extended reals.
- continuous and continuos_on from Multivariate_Analysis:
- "continuous" is the continuity of a function at a filter.
- "isCont" is now an abbrevitation: "isCont x f == continuous (at _) f".
-
- Generalized continuity lemmas from isCont to continuous on an arbitrary
- filter.
-
- - compact from Multivariate_Analysis. Use Bolzano's lemma
- to prove compactness of closed intervals on reals. Continuous functions
- attain infimum and supremum on compact sets. The inverse of a continuous
- function is continuous, when the function is continuous on a compact set.
+ "continuous" is the continuity of a function at a filter. "isCont"
+ is now an abbrevitation: "isCont x f == continuous (at _) f".
+
+ Generalized continuity lemmas from isCont to continuous on an
+ arbitrary filter.
+
+ - compact from Multivariate_Analysis. Use Bolzano's lemma to prove
+ compactness of closed intervals on reals. Continuous functions
+ attain infimum and supremum on compact sets. The inverse of a
+ continuous function is continuous, when the function is continuous
+ on a compact set.
- connected from Multivariate_Analysis. Use it to prove the
intermediate value theorem. Show connectedness of intervals on
linear_continuum_topology).
- first_countable_topology from Multivariate_Analysis. Is used to
- show equivalence of properties on the neighbourhood filter of x and on
- all sequences converging to x.
-
- - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems
- from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on
- FDERIV. Add variants of DERIV and FDERIV which are restricted to sets,
- i.e. to represent derivatives from left or right.
+ show equivalence of properties on the neighbourhood filter of x and
+ on all sequences converging to x.
+
+ - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved
+ theorems from Library/FDERIV.thy to Deriv.thy and base the
+ definition of DERIV on FDERIV. Add variants of DERIV and FDERIV
+ which are restricted to sets, i.e. to represent derivatives from
+ left or right.
- Removed the within-filter. It is replaced by the principal filter:
@@ -323,12 +324,12 @@
- Introduce "at x within U" as a single constant, "at x" is now an
abbreviation for "at x within UNIV"
- - Introduce named theorem collections tendsto_intros, continuous_intros,
- continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or
- FDERIV_intros) are also available as tendsto_eq_intros (or
- FDERIV_eq_intros) where the right-hand side is replaced by a congruence
- rule. This allows to apply them as intro rules and then proving
- equivalence by the simplifier.
+ - Introduce named theorem collections tendsto_intros,
+ continuous_intros, continuous_on_intros and FDERIV_intros. Theorems
+ in tendsto_intros (or FDERIV_intros) are also available as
+ tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side
+ is replaced by a congruence rule. This allows to apply them as
+ intro rules and then proving equivalence by the simplifier.
- Restructured theories in HOL-Complex_Main:
@@ -339,8 +340,8 @@
+ Renamed RealVector to Real_Vector_Spaces
- + Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and
- Limits
+ + Split Lim, SEQ, Series into Topological_Spaces,
+ Real_Vector_Spaces, and Limits
+ Moved Ln and Log to Transcendental
@@ -373,10 +374,10 @@
longer included by default. INCOMPATIBILITY, use partial_function
instead, or import theory Legacy_Mrec as a fallback.
-* HOL-Algebra: Discontinued theories src/HOL/Algebra/abstract and
-.../poly. Existing theories should be based on
-src/HOL/Library/Polynomial instead. The latter provides integration
-with HOL's type classes for rings. INCOMPATIBILITY.
+* HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and
+~~/src/HOL/Algebra/poly. Existing theories should be based on
+~~/src/HOL/Library/Polynomial instead. The latter provides
+integration with HOL's type classes for rings. INCOMPATIBILITY.
*** ML ***