1.1 --- a/NEWS Mon Nov 23 15:11:21 2009 +0100
1.2 +++ b/NEWS Mon Nov 23 16:15:39 2009 +0100
1.3 @@ -55,6 +55,16 @@
1.4 relational model finder. See src/HOL/Tools/Nitpick and
1.5 src/HOL/Nitpick_Examples.
1.6
1.7 +* New commands 'code_pred' and 'values' to invoke the predicate
1.8 +compiler and to enumerate values of inductive predicates.
1.9 +
1.10 +* A tabled implementation of the reflexive transitive closure.
1.11 +
1.12 +* New implementation of quickcheck uses generic code generator;
1.13 +default generators are provided for all suitable HOL types, records
1.14 +and datatypes. Old quickcheck can be re-activated importing theory
1.15 +Library/SML_Quickcheck.
1.16 +
1.17 * New testing tool Mirabelle for automated proof tools. Applies
1.18 several tools and tactics like sledgehammer, metis, or quickcheck, to
1.19 every proof step in a theory. To be used in batch mode via the
1.20 @@ -71,25 +81,9 @@
1.21 to call an external tool every time the proof is checked. See
1.22 src/HOL/Library/Sum_Of_Squares.
1.23
1.24 -* New commands 'code_pred' and 'values' to invoke the predicate
1.25 -compiler and to enumerate values of inductive predicates.
1.26 -
1.27 -* A tabled implementation of the reflexive transitive closure.
1.28 -
1.29 -* New theory SupInf of the supremum and infimum operators for sets of
1.30 -reals.
1.31 -
1.32 -* New theory Probability, which contains a development of measure
1.33 -theory, eventually leading to Lebesgue integration and probability.
1.34 -
1.35 * New method "linarith" invokes existing linear arithmetic decision
1.36 procedure only.
1.37
1.38 -* New implementation of quickcheck uses generic code generator;
1.39 -default generators are provided for all suitable HOL types, records
1.40 -and datatypes. Old quickcheck can be re-activated importing theory
1.41 -Library/SML_Quickcheck.
1.42 -
1.43 * New command 'atp_minimal' reduces result produced by Sledgehammer.
1.44
1.45 * New Sledgehammer option "Full Types" in Proof General settings menu.
1.46 @@ -110,8 +104,14 @@
1.47 * ML antiquotation @{code_datatype} inserts definition of a datatype
1.48 generated by the code generator; e.g. see src/HOL/Predicate.thy.
1.49
1.50 -* Most rules produced by inductive and datatype package have mandatory
1.51 -prefixes. INCOMPATIBILITY.
1.52 +* New theory SupInf of the supremum and infimum operators for sets of
1.53 +reals.
1.54 +
1.55 +* New theory Probability, which contains a development of measure
1.56 +theory, eventually leading to Lebesgue integration and probability.
1.57 +
1.58 +* Extended Multivariate Analysis to include derivation and Brouwer's
1.59 +fixpoint theorem.
1.60
1.61 * Reorganization of number theory, INCOMPATIBILITY:
1.62 - new number theory development for nat and int, in
1.63 @@ -125,7 +125,7 @@
1.64 - moved theory Pocklington from src/HOL/Library to
1.65 src/HOL/Old_Number_Theory
1.66
1.67 -* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
1.68 +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
1.69 of finite and infinite sets. It is shown that they form a complete
1.70 lattice.
1.71
1.72 @@ -137,24 +137,6 @@
1.73 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
1.74 INCOMPATIBILITY.
1.75
1.76 -* Extended Multivariate Analysis to include derivation and Brouwer's
1.77 -fixpoint theorem.
1.78 -
1.79 -* Removed predicate "M hassize n" (<--> card M = n & finite M).
1.80 -INCOMPATIBILITY.
1.81 -
1.82 -* Renamed vector_less_eq_def to vector_le_def, the more usual name.
1.83 -INCOMPATIBILITY.
1.84 -
1.85 -* Added theorem List.map_map as [simp]. Removed List.map_compose.
1.86 -INCOMPATIBILITY.
1.87 -
1.88 -* Code generator attributes follow the usual underscore convention:
1.89 - code_unfold replaces code unfold
1.90 - code_post replaces code post
1.91 - etc.
1.92 - INCOMPATIBILITY.
1.93 -
1.94 * Refinements to lattice classes and sets:
1.95 - less default intro/elim rules in locale variant, more default
1.96 intro/elim rules in class variant: more uniformity
1.97 @@ -165,27 +147,24 @@
1.98 - renamed ACI to inf_sup_aci
1.99 - new class "boolean_algebra"
1.100 - class "complete_lattice" moved to separate theory
1.101 - "complete_lattice"; corresponding constants (and abbreviations)
1.102 + "Complete_Lattice"; corresponding constants (and abbreviations)
1.103 renamed and with authentic syntax:
1.104 - Set.Inf ~> Complete_Lattice.Inf
1.105 - Set.Sup ~> Complete_Lattice.Sup
1.106 - Set.INFI ~> Complete_Lattice.INFI
1.107 - Set.SUPR ~> Complete_Lattice.SUPR
1.108 - Set.Inter ~> Complete_Lattice.Inter
1.109 - Set.Union ~> Complete_Lattice.Union
1.110 - Set.INTER ~> Complete_Lattice.INTER
1.111 - Set.UNION ~> Complete_Lattice.UNION
1.112 - - more convenient names for set intersection and union:
1.113 - Set.Int ~> Set.inter
1.114 - Set.Un ~> Set.union
1.115 + Set.Inf ~> Complete_Lattice.Inf
1.116 + Set.Sup ~> Complete_Lattice.Sup
1.117 + Set.INFI ~> Complete_Lattice.INFI
1.118 + Set.SUPR ~> Complete_Lattice.SUPR
1.119 + Set.Inter ~> Complete_Lattice.Inter
1.120 + Set.Union ~> Complete_Lattice.Union
1.121 + Set.INTER ~> Complete_Lattice.INTER
1.122 + Set.UNION ~> Complete_Lattice.UNION
1.123 - authentic syntax for
1.124 Set.Pow
1.125 Set.image
1.126 - mere abbreviations:
1.127 Set.empty (for bot)
1.128 Set.UNIV (for top)
1.129 - Set.inter (for inf)
1.130 - Set.union (for sup)
1.131 + Set.inter (for inf, formerly Set.Int)
1.132 + Set.union (for sup, formerly Set.Un)
1.133 Complete_Lattice.Inter (for Inf)
1.134 Complete_Lattice.Union (for Sup)
1.135 Complete_Lattice.INTER (for INFI)
1.136 @@ -219,31 +198,47 @@
1.137 abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
1.138 INCOMPATIBILITY.
1.139
1.140 -* Renamed theorems:
1.141 -Suc_eq_add_numeral_1 -> Suc_eq_plus1
1.142 -Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
1.143 -Suc_plus1 -> Suc_eq_plus1
1.144 +--
1.145 +
1.146 +* Most rules produced by inductive and datatype package have mandatory
1.147 +prefixes. INCOMPATIBILITY.
1.148
1.149 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by
1.150 the attribute of the same name. Each of the theorems in the list
1.151 DERIV_intros assumes composition with an additional function and
1.152 matches a variable to the derivative, which has to be solved by the
1.153 Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
1.154 -of most elementary terms.
1.155 -
1.156 -* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
1.157 -are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
1.158 +of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
1.159 +should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
1.160 +
1.161 +* Code generator attributes follow the usual underscore convention:
1.162 + code_unfold replaces code unfold
1.163 + code_post replaces code post
1.164 + etc.
1.165 + INCOMPATIBILITY.
1.166
1.167 * Renamed methods:
1.168 sizechange -> size_change
1.169 induct_scheme -> induction_schema
1.170 -
1.171 -* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
1.172 -INCOMPATIBILITY.
1.173 + INCOMPATIBILITY.
1.174
1.175 * Discontinued abbreviation "arbitrary" of constant "undefined".
1.176 INCOMPATIBILITY, use "undefined" directly.
1.177
1.178 +* Renamed theorems:
1.179 + Suc_eq_add_numeral_1 -> Suc_eq_plus1
1.180 + Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
1.181 + Suc_plus1 -> Suc_eq_plus1
1.182 + *anti_sym -> *antisym*
1.183 + vector_less_eq_def -> vector_le_def
1.184 + INCOMPATIBILITY.
1.185 +
1.186 +* Added theorem List.map_map as [simp]. Removed List.map_compose.
1.187 +INCOMPATIBILITY.
1.188 +
1.189 +* Removed predicate "M hassize n" (<--> card M = n & finite M).
1.190 +INCOMPATIBILITY.
1.191 +
1.192
1.193 *** HOLCF ***
1.194