merged
authorhaftmann
Mon Nov 23 16:15:39 2009 +0100 (2009-11-23)
changeset 3386139c939449d06
parent 33859 033ce4cafba6
parent 33860 dcd9affbd106
child 33862 fb95d9152fa9
merged
     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