--- a/NEWS Wed May 02 20:15:31 2012 +0200
+++ b/NEWS Wed May 02 20:31:15 2012 +0200
@@ -47,10 +47,8 @@
* Bundled declarations associate attributed fact expressions with a
given name in the context. These may be later included in other
contexts. This allows to manage context extensions casually, without
-the logical dependencies of locales and locale interpretation.
-
-See commands 'bundle', 'include', 'including' etc. in the isar-ref
-manual.
+the logical dependencies of locales and locale interpretation. See
+commands 'bundle', 'include', 'including' etc. in the isar-ref manual.
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
@@ -91,6 +89,11 @@
into the user context. Minor INCOMPATIBILITY, may use the regular
"def" result with attribute "abs_def" to imitate the old version.
+* Attribute "abs_def" turns an equation of the form "f x y == t" into
+"f == %x y. t", which ensures that "simp" or "unfold" steps always
+expand it. This also works for object-logic equality. (Formerly
+undocumented feature.)
+
* Renamed some inner syntax categories:
num ~> num_token
@@ -105,11 +108,6 @@
"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
manual. Minor INCOMPATIBILITY.
-* Attribute "abs_def" turns an equation of the form "f x y == t" into
-"f == %x y. t", which ensures that "simp" or "unfold" steps always
-expand it. This also works for object-logic equality. (Formerly
-undocumented feature.)
-
* Obsolete command 'types' has been discontinued. Use 'type_synonym'
instead. INCOMPATIBILITY.
@@ -136,29 +134,38 @@
lemma "P (x::'a)" and "Q (y::'a::bar)"
-- "now uniform 'a::bar instead of default sort for first occurrence (!)"
+* Discontinued configuration option "syntax_positions": atomic terms
+in parse trees are always annotated by position constraints.
+
*** HOL ***
* Type 'a set is now a proper type constructor (just as before
Isabelle2008). Definitions mem_def and Collect_def have disappeared.
Non-trivial INCOMPATIBILITY. For developments keeping predicates and
-sets separate, it is often sufficient to rephrase sets S accidentally
-used as predicates by "%x. x : S" and predicates P accidentally used
-as sets by "{x. P x}". Corresponding proofs in a first step should be
-pruned from any tinkering with former theorems mem_def and Collect_def
-as far as possible.
-
-For developments which deliberately mixed predicates and sets, a
+sets separate, it is often sufficient to rephrase some set S that has
+been accidentally used as predicates by "%x. x : S", and some
+predicate P that has been accidentally used as set by "{x. P x}".
+Corresponding proofs in a first step should be pruned from any
+tinkering with former theorems mem_def and Collect_def as far as
+possible.
+
+For developments which deliberately mix predicates and sets, a
planning step is necessary to determine what should become a predicate
and what a set. It can be helpful to carry out that step in
Isabelle2011-1 before jumping right into the current release.
+* Code generation by default implements sets as container type rather
+than predicates. INCOMPATIBILITY.
+
+* New type synonym 'a rel = ('a * 'a) set
+
* The representation of numerals has changed. Datatype "num"
represents strictly positive binary numerals, along with functions
"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent
-positive and negated numeric literals, respectively. (See definitions
-in ~~/src/HOL/Num.thy.) Potential INCOMPATIBILITY, some user theories
-may require adaptations as follows:
+positive and negated numeric literals, respectively. See also
+definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some
+user theories may require adaptations as follows:
- Theorems with number_ring or number_semiring constraints: These
classes are gone; use comm_ring_1 or comm_semiring_1 instead.
@@ -177,18 +184,8 @@
- Definitions and theorems using old constructors Pls/Min/Bit0/Bit1:
Redefine using other integer operations.
-* Code generation by default implements sets as container type rather
-than predicates. INCOMPATIBILITY.
-
* Records: code generation can be switched off manually with
-declare [[record_coden = false]]. Default remains true.
-
-* HOL-Import: Re-implementation from scratch is faster, simpler, and
-more scalable. Requires a proof bundle, which is available as an
-external component. Discontinued old (and mostly dead) Importer for
-HOL4 and HOL Light. INCOMPATIBILITY.
-
-* New type synonym 'a rel = ('a * 'a) set
+declare [[record_coden = false]]. Default remains true.
* New "case_product" attribute to generate a case rule doing multiple
case distinctions at the same time. E.g.
@@ -198,11 +195,11 @@
produces a rule which can be used to perform case distinction on both
a list and a nat.
-* Transfer: New package intended to generalize the existing descending
-method and related theorem attributes from the Quotient package. (Not
-all functionality is implemented yet, but future development will
-focus on Transfer as an eventual replacement for the corresponding
-parts of the Quotient package.)
+* Transfer: New package intended to generalize the existing
+"descending" method and related theorem attributes from the Quotient
+package. (Not all functionality is implemented yet, but future
+development will focus on Transfer as an eventual replacement for the
+corresponding parts of the Quotient package.)
- transfer_rule attribute: Maintains a collection of transfer rules,
which relate constants at two different types. Transfer rules may
@@ -218,7 +215,7 @@
replaced with corresponding ones according to the transfer rules.
Goals are generalized over all free variables by default; this is
necessary for variables whose types change, but can be overridden
- for specific variables with e.g. 'transfer fixing: x y z'. The
+ for specific variables with e.g. "transfer fixing: x y z". The
variant transfer' method allows replacing a subgoal with one that
is logically stronger (rather than equivalent).
@@ -317,9 +314,8 @@
- Added "quickcheck_locale" configuration to specify how to process
conjectures in a locale context.
-* Nitpick:
- - Fixed infinite loop caused by the 'peephole_optim' option and
- affecting 'rat' and 'real'.
+* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option
+and affecting 'rat' and 'real'.
* Sledgehammer:
- Integrated more tightly with SPASS, as described in the ITP 2012
@@ -333,23 +329,31 @@
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
- Renamed "sound" option to "strict".
-* Metis:
- - Added possibility to specify lambda translations scheme as a
- parenthesized argument (e.g., "by (metis (lifting) ...)").
-
-* SMT:
- - Renamed "smt_fixed" option to "smt_read_only_certificates".
-
-* Command 'try0':
- - Renamed from 'try_methods'. INCOMPATIBILITY.
+* Metis: Added possibility to specify lambda translations scheme as a
+parenthesized argument (e.g., "by (metis (lifting) ...)").
+
+* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates".
+
+* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY.
* New "eventually_elim" method as a generalized variant of the
-eventually_elim* rules. Supports structured proofs.
+eventually_elim* rules. Supports structured proofs.
+
+* 'datatype' specifications allow explicit sort constraints.
* Typedef with implicit set definition is considered legacy. Use
"typedef (open)" form instead, which will eventually become the
default.
+* Concrete syntax for case expressions includes constraints for source
+positions, and thus produces Prover IDE markup for its bindings.
+INCOMPATIBILITY for old-style syntax translations that augment the
+pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
+one_case.
+
+* Clarified attribute "mono_set": pure declaration without modifying
+the result of the fact expression.
+
* More default pred/set conversions on a couple of relation operations
and predicates. Added powers of predicate relations. Consolidation
of some relation theorems:
@@ -512,16 +516,7 @@
* Congruence rules Option.map_cong and Option.bind_cong for recursion
through option types.
-* Concrete syntax for case expressions includes constraints for source
-positions, and thus produces Prover IDE markup for its bindings.
-INCOMPATIBILITY for old-style syntax translations that augment the
-pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
-one_case.
-
-* Discontinued configuration option "syntax_positions": atomic terms
-in parse trees are always annotated by position constraints.
-
-* HOL/Library/Set_Algebras.thy: Addition and multiplication on sets
+* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets
are expressed via type classes again. The special syntax
\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant
setsum_set, which is now subsumed by Big_Operators.setsum.
@@ -530,8 +525,6 @@
* New theory HOL/Library/DAList provides an abstract type for
association lists with distinct keys.
-* 'datatype' specifications allow explicit sort constraints.
-
* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY,
use theory HOL/Library/Nat_Bijection instead.
@@ -711,55 +704,6 @@
real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl,
round_up, zero_le_float, zero_less_float
-* Session HOL-Word: Discontinued many redundant theorems specific to
-type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
-instead.
-
- word_sub_alt ~> word_sub_wi
- word_add_alt ~> word_add_def
- word_mult_alt ~> word_mult_def
- word_minus_alt ~> word_minus_def
- word_0_alt ~> word_0_wi
- word_1_alt ~> word_1_wi
- word_add_0 ~> add_0_left
- word_add_0_right ~> add_0_right
- word_mult_1 ~> mult_1_left
- word_mult_1_right ~> mult_1_right
- word_add_commute ~> add_commute
- word_add_assoc ~> add_assoc
- word_add_left_commute ~> add_left_commute
- word_mult_commute ~> mult_commute
- word_mult_assoc ~> mult_assoc
- word_mult_left_commute ~> mult_left_commute
- word_left_distrib ~> left_distrib
- word_right_distrib ~> right_distrib
- word_left_minus ~> left_minus
- word_diff_0_right ~> diff_0_right
- word_diff_self ~> diff_self
- word_sub_def ~> diff_minus
- word_diff_minus ~> diff_minus
- word_add_ac ~> add_ac
- word_mult_ac ~> mult_ac
- word_plus_ac0 ~> add_0_left add_0_right add_ac
- word_times_ac1 ~> mult_1_left mult_1_right mult_ac
- word_order_trans ~> order_trans
- word_order_refl ~> order_refl
- word_order_antisym ~> order_antisym
- word_order_linear ~> linorder_linear
- lenw1_zero_neq_one ~> zero_neq_one
- word_number_of_eq ~> number_of_eq
- word_of_int_add_hom ~> wi_hom_add
- word_of_int_sub_hom ~> wi_hom_sub
- word_of_int_mult_hom ~> wi_hom_mult
- word_of_int_minus_hom ~> wi_hom_neg
- word_of_int_succ_hom ~> wi_hom_succ
- word_of_int_pred_hom ~> wi_hom_pred
- word_of_int_0_hom ~> word_0_wi
- word_of_int_1_hom ~> word_1_wi
-
-* Clarified attribute "mono_set": pure declaration without modifying
-the result of the fact expression.
-
* "Transitive_Closure.ntrancl": bounded transitive closure on
relations.
@@ -807,6 +751,57 @@
DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing
+* Session HOL-Import: Re-implementation from scratch is faster,
+simpler, and more scalable. Requires a proof bundle, which is
+available as an external component. Discontinued old (and mostly
+dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY.
+
+* Session HOL-Word: Discontinued many redundant theorems specific to
+type 'a word. INCOMPATIBILITY, use the corresponding generic theorems
+instead.
+
+ word_sub_alt ~> word_sub_wi
+ word_add_alt ~> word_add_def
+ word_mult_alt ~> word_mult_def
+ word_minus_alt ~> word_minus_def
+ word_0_alt ~> word_0_wi
+ word_1_alt ~> word_1_wi
+ word_add_0 ~> add_0_left
+ word_add_0_right ~> add_0_right
+ word_mult_1 ~> mult_1_left
+ word_mult_1_right ~> mult_1_right
+ word_add_commute ~> add_commute
+ word_add_assoc ~> add_assoc
+ word_add_left_commute ~> add_left_commute
+ word_mult_commute ~> mult_commute
+ word_mult_assoc ~> mult_assoc
+ word_mult_left_commute ~> mult_left_commute
+ word_left_distrib ~> left_distrib
+ word_right_distrib ~> right_distrib
+ word_left_minus ~> left_minus
+ word_diff_0_right ~> diff_0_right
+ word_diff_self ~> diff_self
+ word_sub_def ~> diff_minus
+ word_diff_minus ~> diff_minus
+ word_add_ac ~> add_ac
+ word_mult_ac ~> mult_ac
+ word_plus_ac0 ~> add_0_left add_0_right add_ac
+ word_times_ac1 ~> mult_1_left mult_1_right mult_ac
+ word_order_trans ~> order_trans
+ word_order_refl ~> order_refl
+ word_order_antisym ~> order_antisym
+ word_order_linear ~> linorder_linear
+ lenw1_zero_neq_one ~> zero_neq_one
+ word_number_of_eq ~> number_of_eq
+ word_of_int_add_hom ~> wi_hom_add
+ word_of_int_sub_hom ~> wi_hom_sub
+ word_of_int_mult_hom ~> wi_hom_mult
+ word_of_int_minus_hom ~> wi_hom_neg
+ word_of_int_succ_hom ~> wi_hom_succ
+ word_of_int_pred_hom ~> wi_hom_pred
+ word_of_int_0_hom ~> word_0_wi
+ word_of_int_1_hom ~> word_1_wi
+
* Theory Library/Multiset: Improved code generation of multisets.
* Session HOL-Word: New proof method "word_bitwise" for splitting
@@ -991,8 +986,8 @@
sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq
space_product_algebra -> space_PiM
-* HOL/TPTP: support to parse and import TPTP problems (all languages)
-into Isabelle/HOL.
+* Session HOL-TPTP: support to parse and import TPTP problems (all
+languages) into Isabelle/HOL.
*** FOL ***