summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Wed, 12 May 2010 13:34:24 +0200 | |

changeset 36857 | 59ed53700145 |

parent 36856 | b343091e81d8 |

child 36858 | 8eac822dec6c |

child 36868 | b78d3c87fc88 |

minor tuning;

--- a/NEWS Wed May 12 13:21:23 2010 +0200 +++ b/NEWS Wed May 12 13:34:24 2010 +0200 @@ -73,14 +73,14 @@ discontinued (legacy feature). * References 'trace_simp' and 'debug_simp' have been replaced by -configuration options stored in the context. Enabling tracing -(the case of debugging is similar) in proofs works via - - using [[trace_simp=true]] - -Tracing is then active for all invocations of the simplifier -in subsequent goal refinement steps. Tracing may also still be -enabled or disabled via the ProofGeneral settings menu. +configuration options stored in the context. Enabling tracing (the +case of debugging is similar) in proofs works via + + using [[trace_simp = true]] + +Tracing is then active for all invocations of the simplifier in +subsequent goal refinement steps. Tracing may also still be enabled or +disabled via the ProofGeneral settings menu. * Separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact' replace the former 'hide' KIND command. Minor @@ -89,18 +89,20 @@ *** Pure *** -* Predicates of locales introduces by classes carry a mandatory "class" -prefix. INCOMPATIBILITY. - -* 'code_reflect' allows to incorporate generated ML code into -runtime environment; replaces immature code_datatype antiquotation. +* Predicates of locales introduces by classes carry a mandatory +"class" prefix. INCOMPATIBILITY. + +* Command 'code_reflect' allows to incorporate generated ML code into +runtime environment; replaces immature code_datatype antiquotation. INCOMPATIBILITY. * Empty class specifications observe default sort. INCOMPATIBILITY. -* Old 'axclass' has been discontinued. Use 'class' instead. INCOMPATIBILITY. - -* Code generator: simple concept for abstract datatypes obeying invariants. +* Old 'axclass' command has been discontinued. Use 'class' instead. +INCOMPATIBILITY. + +* Code generator: simple concept for abstract datatypes obeying +invariants. * Local theory specifications may depend on extra type variables that are not present in the result type -- arguments TYPE('a) :: 'a itself @@ -108,11 +110,12 @@ definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)" -* Code generator: details of internal data cache have no impact on -the user space functionality any longer. - -* Methods unfold_locales and intro_locales ignore non-locale subgoals. This -is more appropriate for interpretations with 'where'. INCOMPATIBILITY. +* Code generator: details of internal data cache have no impact on the +user space functionality any longer. + +* Methods unfold_locales and intro_locales ignore non-locale subgoals. +This is more appropriate for interpretations with 'where'. +INCOMPATIBILITY. * Discontinued unnamed infix syntax (legacy feature for many years) -- need to specify constant name and syntax separately. Internal ML @@ -130,18 +133,18 @@ context -- without introducing dependencies on parameters or assumptions, which is not possible in Isabelle/Pure. -* Command 'defaultsort' is renamed to 'default_sort', it works within -a local theory context. Minor INCOMPATIBILITY. +* Command 'defaultsort' has been renamed to 'default_sort', it works +within a local theory context. Minor INCOMPATIBILITY. * Proof terms: Type substitutions on proof constants now use canonical -order of type variables. INCOMPATIBILITY: Tools working with proof -terms may need to be adapted. +order of type variables. Potential INCOMPATIBILITY for tools working +with proof terms. *** HOL *** -* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is -no longer shadowed. INCOMPATIBILITY. +* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no +longer shadowed. INCOMPATIBILITY. * Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY. @@ -149,15 +152,15 @@ * Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead. INCOMPATIBILITY. -* Dropped normalizing_semiring etc; use the facts in semiring classes instead. -INCOMPATIBILITY. - -* Theory 'Finite_Set': various folding_* locales facilitate the application -of the various fold combinators on finite sets. - -* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT' -provides abstract red-black tree type which is backed by RBT_Impl -as implementation. INCOMPATIBILTY. +* Dropped normalizing_semiring etc; use the facts in semiring classes +instead. INCOMPATIBILITY. + +* Theory 'Finite_Set': various folding_XXX locales facilitate the +application of the various fold combinators on finite sets. + +* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT" +provides abstract red-black tree type which is backed by "RBT_Impl" as +implementation. INCOMPATIBILTY. * Command 'typedef' now works within a local theory context -- without introducing dependencies on parameters or assumptions, which is not @@ -171,27 +174,28 @@ * Theory PReal, including the type "preal" and related operations, has been removed. INCOMPATIBILITY. -* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, -Min, Max from theory Finite_Set. INCOMPATIBILITY. - -* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. -INCOMPATIBILITY. - -* New set of rules "ac_simps" provides combined assoc / commute rewrites -for all interpretations of the appropriate generic locales. - -* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field" -into theories "Rings" and "Fields"; for more appropriate and more -consistent names suitable for name prefixes within the HOL theories. -INCOMPATIBILITY. +* Split off theory Big_Operators containing setsum, setprod, Inf_fin, +Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. + +* Theory "Rational" renamed to "Rat", for consistency with "Nat", +"Int" etc. INCOMPATIBILITY. + +* New set of rules "ac_simps" provides combined assoc / commute +rewrites for all interpretations of the appropriate generic locales. + +* Renamed theory "OrderedGroup" to "Groups" and split theory +"Ring_and_Field" into theories "Rings" and "Fields"; for more +appropriate and more consistent names suitable for name prefixes +within the HOL theories. INCOMPATIBILITY. * Some generic constants have been put to appropriate theories: - * less_eq, less: Orderings - * zero, one, plus, minus, uminus, times, abs, sgn: Groups - * inverse, divide: Rings + - less_eq, less: Orderings + - zero, one, plus, minus, uminus, times, abs, sgn: Groups + - inverse, divide: Rings INCOMPATIBILITY. -* More consistent naming of type classes involving orderings (and lattices): +* More consistent naming of type classes involving orderings (and +lattices): lower_semilattice ~> semilattice_inf upper_semilattice ~> semilattice_sup @@ -231,8 +235,8 @@ ordered_semiring_1_strict ~> linordered_semiring_1_strict ordered_semiring_strict ~> linordered_semiring_strict - The following slightly odd type classes have been moved to - a separate theory Library/Lattice_Algebras.thy: + The following slightly odd type classes have been moved to a + separate theory Library/Lattice_Algebras.thy: lordered_ab_group_add ~> lattice_ab_group_add lordered_ab_group_add_abs ~> lattice_ab_group_add_abs @@ -243,17 +247,20 @@ INCOMPATIBILITY. * Refined field classes: - * classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero - include rule inverse 0 = 0 -- subsumes former division_by_zero class. - * numerous lemmas have been ported from field to division_ring; - INCOMPATIBILITY. + - classes division_ring_inverse_zero, field_inverse_zero, + linordered_field_inverse_zero include rule inverse 0 = 0 -- + subsumes former division_by_zero class; + - numerous lemmas have been ported from field to division_ring. +INCOMPATIBILITY. * Refined algebra theorem collections: - * dropped theorem group group_simps, use algebra_simps instead; - * dropped theorem group ring_simps, use field_simps instead; - * proper theorem collection field_simps subsumes former theorem groups field_eq_simps and field_simps; - * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero. - INCOMPATIBILITY. + - dropped theorem group group_simps, use algebra_simps instead; + - dropped theorem group ring_simps, use field_simps instead; + - proper theorem collection field_simps subsumes former theorem + groups field_eq_simps and field_simps; + - dropped lemma eq_minus_self_iff which is a duplicate for + equal_neg_zero. +INCOMPATIBILITY. * Theory Finite_Set and List: some lemmas have been generalized from sets to lattices: @@ -279,14 +286,19 @@ * HOLogic.strip_psplit: types are returned in syntactic order, similar to other strip and tuple operations. INCOMPATIBILITY. -* Reorganized theory Multiset: swapped notation of pointwise and multiset order: - * pointwise ordering is instance of class order with standard syntax <= and <; - * multiset ordering has syntax <=# and <#; partial order properties are provided - by means of interpretation with prefix multiset_order; - * less duplication, less historical organization of sections, - conversion from associations lists to multisets, rudimentary code generation; - * use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. - INCOMPATIBILITY. +* Reorganized theory Multiset: swapped notation of pointwise and +multiset order: + - pointwise ordering is instance of class order with standard syntax + <= and <; + - multiset ordering has syntax <=# and <#; partial order properties + are provided by means of interpretation with prefix + multiset_order; + - less duplication, less historical organization of sections, + conversion from associations lists to multisets, rudimentary code + generation; + - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, + if needed. +INCOMPATIBILITY. * Code generation: ML and OCaml code is decorated with signatures.