# HG changeset patch # User haftmann # Date 1258989339 -3600 # Node ID 39c939449d06e1fa3721ff047c6b9f4da5b56a3d # Parent 033ce4cafba647ec58475782de46c6f6cf435ae3# Parent dcd9affbd1064844c44712eb03e2eac6df9d64a4 merged diff -r 033ce4cafba6 -r 39c939449d06 NEWS --- a/NEWS Mon Nov 23 15:11:21 2009 +0100 +++ b/NEWS Mon Nov 23 16:15:39 2009 +0100 @@ -55,6 +55,16 @@ relational model finder. See src/HOL/Tools/Nitpick and src/HOL/Nitpick_Examples. +* New commands 'code_pred' and 'values' to invoke the predicate +compiler and to enumerate values of inductive predicates. + +* A tabled implementation of the reflexive transitive closure. + +* New implementation of quickcheck uses generic code generator; +default generators are provided for all suitable HOL types, records +and datatypes. Old quickcheck can be re-activated importing theory +Library/SML_Quickcheck. + * New testing tool Mirabelle for automated proof tools. Applies several tools and tactics like sledgehammer, metis, or quickcheck, to every proof step in a theory. To be used in batch mode via the @@ -71,25 +81,9 @@ to call an external tool every time the proof is checked. See src/HOL/Library/Sum_Of_Squares. -* New commands 'code_pred' and 'values' to invoke the predicate -compiler and to enumerate values of inductive predicates. - -* A tabled implementation of the reflexive transitive closure. - -* New theory SupInf of the supremum and infimum operators for sets of -reals. - -* New theory Probability, which contains a development of measure -theory, eventually leading to Lebesgue integration and probability. - * New method "linarith" invokes existing linear arithmetic decision procedure only. -* New implementation of quickcheck uses generic code generator; -default generators are provided for all suitable HOL types, records -and datatypes. Old quickcheck can be re-activated importing theory -Library/SML_Quickcheck. - * New command 'atp_minimal' reduces result produced by Sledgehammer. * New Sledgehammer option "Full Types" in Proof General settings menu. @@ -110,8 +104,14 @@ * ML antiquotation @{code_datatype} inserts definition of a datatype generated by the code generator; e.g. see src/HOL/Predicate.thy. -* Most rules produced by inductive and datatype package have mandatory -prefixes. INCOMPATIBILITY. +* New theory SupInf of the supremum and infimum operators for sets of +reals. + +* New theory Probability, which contains a development of measure +theory, eventually leading to Lebesgue integration and probability. + +* Extended Multivariate Analysis to include derivation and Brouwer's +fixpoint theorem. * Reorganization of number theory, INCOMPATIBILITY: - new number theory development for nat and int, in @@ -125,7 +125,7 @@ - moved theory Pocklington from src/HOL/Library to src/HOL/Old_Number_Theory -* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and infinite sets. It is shown that they form a complete lattice. @@ -137,24 +137,6 @@ zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. -* Extended Multivariate Analysis to include derivation and Brouwer's -fixpoint theorem. - -* Removed predicate "M hassize n" (<--> card M = n & finite M). -INCOMPATIBILITY. - -* Renamed vector_less_eq_def to vector_le_def, the more usual name. -INCOMPATIBILITY. - -* Added theorem List.map_map as [simp]. Removed List.map_compose. -INCOMPATIBILITY. - -* Code generator attributes follow the usual underscore convention: - code_unfold replaces code unfold - code_post replaces code post - etc. - INCOMPATIBILITY. - * Refinements to lattice classes and sets: - less default intro/elim rules in locale variant, more default intro/elim rules in class variant: more uniformity @@ -165,27 +147,24 @@ - renamed ACI to inf_sup_aci - new class "boolean_algebra" - class "complete_lattice" moved to separate theory - "complete_lattice"; corresponding constants (and abbreviations) + "Complete_Lattice"; corresponding constants (and abbreviations) renamed and with authentic syntax: - Set.Inf ~> Complete_Lattice.Inf - Set.Sup ~> Complete_Lattice.Sup - Set.INFI ~> Complete_Lattice.INFI - Set.SUPR ~> Complete_Lattice.SUPR - Set.Inter ~> Complete_Lattice.Inter - Set.Union ~> Complete_Lattice.Union - Set.INTER ~> Complete_Lattice.INTER - Set.UNION ~> Complete_Lattice.UNION - - more convenient names for set intersection and union: - Set.Int ~> Set.inter - Set.Un ~> Set.union + Set.Inf ~> Complete_Lattice.Inf + Set.Sup ~> Complete_Lattice.Sup + Set.INFI ~> Complete_Lattice.INFI + Set.SUPR ~> Complete_Lattice.SUPR + Set.Inter ~> Complete_Lattice.Inter + Set.Union ~> Complete_Lattice.Union + Set.INTER ~> Complete_Lattice.INTER + Set.UNION ~> Complete_Lattice.UNION - authentic syntax for Set.Pow Set.image - mere abbreviations: Set.empty (for bot) Set.UNIV (for top) - Set.inter (for inf) - Set.union (for sup) + Set.inter (for inf, formerly Set.Int) + Set.union (for sup, formerly Set.Un) Complete_Lattice.Inter (for Inf) Complete_Lattice.Union (for Sup) Complete_Lattice.INTER (for INFI) @@ -219,31 +198,47 @@ abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. INCOMPATIBILITY. -* Renamed theorems: -Suc_eq_add_numeral_1 -> Suc_eq_plus1 -Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left -Suc_plus1 -> Suc_eq_plus1 +-- + +* Most rules produced by inductive and datatype package have mandatory +prefixes. INCOMPATIBILITY. * Changed "DERIV_intros" to a dynamic fact, which can be augmented by the attribute of the same name. Each of the theorems in the list DERIV_intros assumes composition with an additional function and matches a variable to the derivative, which has to be solved by the Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative -of most elementary terms. - -* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded -are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY. +of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac +should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY. + +* Code generator attributes follow the usual underscore convention: + code_unfold replaces code unfold + code_post replaces code post + etc. + INCOMPATIBILITY. * Renamed methods: sizechange -> size_change induct_scheme -> induction_schema - -* Lemma name change: replaced "anti_sym" by "antisym" everywhere. -INCOMPATIBILITY. + INCOMPATIBILITY. * Discontinued abbreviation "arbitrary" of constant "undefined". INCOMPATIBILITY, use "undefined" directly. +* Renamed theorems: + Suc_eq_add_numeral_1 -> Suc_eq_plus1 + Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left + Suc_plus1 -> Suc_eq_plus1 + *anti_sym -> *antisym* + vector_less_eq_def -> vector_le_def + INCOMPATIBILITY. + +* Added theorem List.map_map as [simp]. Removed List.map_compose. +INCOMPATIBILITY. + +* Removed predicate "M hassize n" (<--> card M = n & finite M). +INCOMPATIBILITY. + *** HOLCF ***