1.1 --- a/NEWS Wed May 12 13:21:23 2010 +0200
1.2 +++ b/NEWS Wed May 12 13:34:24 2010 +0200
1.3 @@ -73,14 +73,14 @@
1.4 discontinued (legacy feature).
1.5
1.6 * References 'trace_simp' and 'debug_simp' have been replaced by
1.7 -configuration options stored in the context. Enabling tracing
1.8 -(the case of debugging is similar) in proofs works via
1.9 -
1.10 - using [[trace_simp=true]]
1.11 -
1.12 -Tracing is then active for all invocations of the simplifier
1.13 -in subsequent goal refinement steps. Tracing may also still be
1.14 -enabled or disabled via the ProofGeneral settings menu.
1.15 +configuration options stored in the context. Enabling tracing (the
1.16 +case of debugging is similar) in proofs works via
1.17 +
1.18 + using [[trace_simp = true]]
1.19 +
1.20 +Tracing is then active for all invocations of the simplifier in
1.21 +subsequent goal refinement steps. Tracing may also still be enabled or
1.22 +disabled via the ProofGeneral settings menu.
1.23
1.24 * Separate commands 'hide_class', 'hide_type', 'hide_const',
1.25 'hide_fact' replace the former 'hide' KIND command. Minor
1.26 @@ -89,18 +89,20 @@
1.27
1.28 *** Pure ***
1.29
1.30 -* Predicates of locales introduces by classes carry a mandatory "class"
1.31 -prefix. INCOMPATIBILITY.
1.32 -
1.33 -* 'code_reflect' allows to incorporate generated ML code into
1.34 -runtime environment; replaces immature code_datatype antiquotation.
1.35 +* Predicates of locales introduces by classes carry a mandatory
1.36 +"class" prefix. INCOMPATIBILITY.
1.37 +
1.38 +* Command 'code_reflect' allows to incorporate generated ML code into
1.39 +runtime environment; replaces immature code_datatype antiquotation.
1.40 INCOMPATIBILITY.
1.41
1.42 * Empty class specifications observe default sort. INCOMPATIBILITY.
1.43
1.44 -* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY.
1.45 -
1.46 -* Code generator: simple concept for abstract datatypes obeying invariants.
1.47 +* Old 'axclass' command has been discontinued. Use 'class' instead.
1.48 +INCOMPATIBILITY.
1.49 +
1.50 +* Code generator: simple concept for abstract datatypes obeying
1.51 +invariants.
1.52
1.53 * Local theory specifications may depend on extra type variables that
1.54 are not present in the result type -- arguments TYPE('a) :: 'a itself
1.55 @@ -108,11 +110,12 @@
1.56
1.57 definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
1.58
1.59 -* Code generator: details of internal data cache have no impact on
1.60 -the user space functionality any longer.
1.61 -
1.62 -* Methods unfold_locales and intro_locales ignore non-locale subgoals. This
1.63 -is more appropriate for interpretations with 'where'. INCOMPATIBILITY.
1.64 +* Code generator: details of internal data cache have no impact on the
1.65 +user space functionality any longer.
1.66 +
1.67 +* Methods unfold_locales and intro_locales ignore non-locale subgoals.
1.68 +This is more appropriate for interpretations with 'where'.
1.69 +INCOMPATIBILITY.
1.70
1.71 * Discontinued unnamed infix syntax (legacy feature for many years) --
1.72 need to specify constant name and syntax separately. Internal ML
1.73 @@ -130,18 +133,18 @@
1.74 context -- without introducing dependencies on parameters or
1.75 assumptions, which is not possible in Isabelle/Pure.
1.76
1.77 -* Command 'defaultsort' is renamed to 'default_sort', it works within
1.78 -a local theory context. Minor INCOMPATIBILITY.
1.79 +* Command 'defaultsort' has been renamed to 'default_sort', it works
1.80 +within a local theory context. Minor INCOMPATIBILITY.
1.81
1.82 * Proof terms: Type substitutions on proof constants now use canonical
1.83 -order of type variables. INCOMPATIBILITY: Tools working with proof
1.84 -terms may need to be adapted.
1.85 +order of type variables. Potential INCOMPATIBILITY for tools working
1.86 +with proof terms.
1.87
1.88
1.89 *** HOL ***
1.90
1.91 -* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
1.92 -no longer shadowed. INCOMPATIBILITY.
1.93 +* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no
1.94 +longer shadowed. INCOMPATIBILITY.
1.95
1.96 * Dropped theorem duplicate comp_arith; use semiring_norm instead.
1.97 INCOMPATIBILITY.
1.98 @@ -149,15 +152,15 @@
1.99 * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
1.100 INCOMPATIBILITY.
1.101
1.102 -* Dropped normalizing_semiring etc; use the facts in semiring classes instead.
1.103 -INCOMPATIBILITY.
1.104 -
1.105 -* Theory 'Finite_Set': various folding_* locales facilitate the application
1.106 -of the various fold combinators on finite sets.
1.107 -
1.108 -* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
1.109 -provides abstract red-black tree type which is backed by RBT_Impl
1.110 -as implementation. INCOMPATIBILTY.
1.111 +* Dropped normalizing_semiring etc; use the facts in semiring classes
1.112 +instead. INCOMPATIBILITY.
1.113 +
1.114 +* Theory 'Finite_Set': various folding_XXX locales facilitate the
1.115 +application of the various fold combinators on finite sets.
1.116 +
1.117 +* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT"
1.118 +provides abstract red-black tree type which is backed by "RBT_Impl" as
1.119 +implementation. INCOMPATIBILTY.
1.120
1.121 * Command 'typedef' now works within a local theory context -- without
1.122 introducing dependencies on parameters or assumptions, which is not
1.123 @@ -171,27 +174,28 @@
1.124 * Theory PReal, including the type "preal" and related operations, has
1.125 been removed. INCOMPATIBILITY.
1.126
1.127 -* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
1.128 -Min, Max from theory Finite_Set. INCOMPATIBILITY.
1.129 -
1.130 -* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
1.131 +* Split off theory Big_Operators containing setsum, setprod, Inf_fin,
1.132 +Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
1.133 +
1.134 +* Theory "Rational" renamed to "Rat", for consistency with "Nat",
1.135 +"Int" etc. INCOMPATIBILITY.
1.136 +
1.137 +* New set of rules "ac_simps" provides combined assoc / commute
1.138 +rewrites for all interpretations of the appropriate generic locales.
1.139 +
1.140 +* Renamed theory "OrderedGroup" to "Groups" and split theory
1.141 +"Ring_and_Field" into theories "Rings" and "Fields"; for more
1.142 +appropriate and more consistent names suitable for name prefixes
1.143 +within the HOL theories. INCOMPATIBILITY.
1.144 +
1.145 +* Some generic constants have been put to appropriate theories:
1.146 + - less_eq, less: Orderings
1.147 + - zero, one, plus, minus, uminus, times, abs, sgn: Groups
1.148 + - inverse, divide: Rings
1.149 INCOMPATIBILITY.
1.150
1.151 -* New set of rules "ac_simps" provides combined assoc / commute rewrites
1.152 -for all interpretations of the appropriate generic locales.
1.153 -
1.154 -* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"
1.155 -into theories "Rings" and "Fields"; for more appropriate and more
1.156 -consistent names suitable for name prefixes within the HOL theories.
1.157 -INCOMPATIBILITY.
1.158 -
1.159 -* Some generic constants have been put to appropriate theories:
1.160 - * less_eq, less: Orderings
1.161 - * zero, one, plus, minus, uminus, times, abs, sgn: Groups
1.162 - * inverse, divide: Rings
1.163 -INCOMPATIBILITY.
1.164 -
1.165 -* More consistent naming of type classes involving orderings (and lattices):
1.166 +* More consistent naming of type classes involving orderings (and
1.167 +lattices):
1.168
1.169 lower_semilattice ~> semilattice_inf
1.170 upper_semilattice ~> semilattice_sup
1.171 @@ -231,8 +235,8 @@
1.172 ordered_semiring_1_strict ~> linordered_semiring_1_strict
1.173 ordered_semiring_strict ~> linordered_semiring_strict
1.174
1.175 - The following slightly odd type classes have been moved to
1.176 - a separate theory Library/Lattice_Algebras.thy:
1.177 + The following slightly odd type classes have been moved to a
1.178 + separate theory Library/Lattice_Algebras.thy:
1.179
1.180 lordered_ab_group_add ~> lattice_ab_group_add
1.181 lordered_ab_group_add_abs ~> lattice_ab_group_add_abs
1.182 @@ -243,17 +247,20 @@
1.183 INCOMPATIBILITY.
1.184
1.185 * Refined field classes:
1.186 - * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
1.187 - include rule inverse 0 = 0 -- subsumes former division_by_zero class.
1.188 - * numerous lemmas have been ported from field to division_ring;
1.189 - INCOMPATIBILITY.
1.190 + - classes division_ring_inverse_zero, field_inverse_zero,
1.191 + linordered_field_inverse_zero include rule inverse 0 = 0 --
1.192 + subsumes former division_by_zero class;
1.193 + - numerous lemmas have been ported from field to division_ring.
1.194 +INCOMPATIBILITY.
1.195
1.196 * Refined algebra theorem collections:
1.197 - * dropped theorem group group_simps, use algebra_simps instead;
1.198 - * dropped theorem group ring_simps, use field_simps instead;
1.199 - * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps;
1.200 - * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
1.201 - INCOMPATIBILITY.
1.202 + - dropped theorem group group_simps, use algebra_simps instead;
1.203 + - dropped theorem group ring_simps, use field_simps instead;
1.204 + - proper theorem collection field_simps subsumes former theorem
1.205 + groups field_eq_simps and field_simps;
1.206 + - dropped lemma eq_minus_self_iff which is a duplicate for
1.207 + equal_neg_zero.
1.208 +INCOMPATIBILITY.
1.209
1.210 * Theory Finite_Set and List: some lemmas have been generalized from
1.211 sets to lattices:
1.212 @@ -279,14 +286,19 @@
1.213 * HOLogic.strip_psplit: types are returned in syntactic order, similar
1.214 to other strip and tuple operations. INCOMPATIBILITY.
1.215
1.216 -* Reorganized theory Multiset: swapped notation of pointwise and multiset order:
1.217 - * pointwise ordering is instance of class order with standard syntax <= and <;
1.218 - * multiset ordering has syntax <=# and <#; partial order properties are provided
1.219 - by means of interpretation with prefix multiset_order;
1.220 - * less duplication, less historical organization of sections,
1.221 - conversion from associations lists to multisets, rudimentary code generation;
1.222 - * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
1.223 - INCOMPATIBILITY.
1.224 +* Reorganized theory Multiset: swapped notation of pointwise and
1.225 +multiset order:
1.226 + - pointwise ordering is instance of class order with standard syntax
1.227 + <= and <;
1.228 + - multiset ordering has syntax <=# and <#; partial order properties
1.229 + are provided by means of interpretation with prefix
1.230 + multiset_order;
1.231 + - less duplication, less historical organization of sections,
1.232 + conversion from associations lists to multisets, rudimentary code
1.233 + generation;
1.234 + - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
1.235 + if needed.
1.236 +INCOMPATIBILITY.
1.237
1.238 * Code generation: ML and OCaml code is decorated with signatures.
1.239