# HG changeset patch # User wenzelm # Date 1334401559 -7200 # Node ID b1cd02f2d534a856c35024c44e75079d0fcefbbb # Parent 9be52539082de657325f87720f505be065326c02 misc tuning for release; diff -r 9be52539082d -r b1cd02f2d534 NEWS --- a/NEWS Sat Apr 14 12:51:38 2012 +0200 +++ b/NEWS Sat Apr 14 13:05:59 2012 +0200 @@ -47,9 +47,6 @@ header -- minor INCOMPATIBILITY for user-defined commands. Allow new commands to be used in the same theory where defined. -* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar -(not just JRE). - *** Pure *** @@ -68,21 +65,21 @@ undocumented feature.) * Discontinued old "prems" fact, which used to refer to the accidental -collection of foundational premises in the context (marked as legacy -since Isabelle2011). +collection of foundational premises in the context (already marked as +legacy since Isabelle2011). * Obsolete command 'types' has been discontinued. Use 'type_synonym' instead. INCOMPATIBILITY. -* Ancient code generator for SML and its commands 'code_module', +* Old code generator for SML and its commands 'code_module', 'code_library', 'consts_code', 'types_code' have been discontinued. Use commands of the generic code generator instead. INCOMPATIBILITY. -* Redundant attribute 'code_inline' has been discontinued. Use -'code_unfold' instead. INCOMPATIBILITY. - -* Dropped attribute 'code_unfold_post' in favor of the its dual -'code_abbrev', which yields a common pattern in definitions like +* Redundant attribute "code_inline" has been discontinued. Use +"code_unfold" instead. INCOMPATIBILITY. + +* Dropped attribute "code_unfold_post" in favor of the its dual +"code_abbrev", which yields a common pattern in definitions like definition [code_abbrev]: "f = t" @@ -100,14 +97,30 @@ *** HOL *** -* New tutorial Programming and Proving in Isabelle/HOL - -* The representation of numerals has changed. We now have a datatype -"num" representing 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 Num.thy.) Potential INCOMPATIBILITY; some user theories -may require adaptations: +* New tutorial Programming and Proving in Isabelle/HOL ("prog-prove"). + +* Discontinued old Tutorial on Isar ("isar-overview"); + +* 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 +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. + +* 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: - Theorems with number_ring or number_semiring constraints: These classes are gone; use comm_ring_1 or comm_semiring_1 instead. @@ -126,25 +139,12 @@ - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: Redefine using other integer operations. -* 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 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 proof import from HOL Light: Faster, simpler, and more scalable. Requires a proof bundle, which is available as an external component. -Removed old (and mostly dead) Importer for HOL4 and HOL Light. +Discontinued old (and mostly dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY. * New type synonym 'a rel = ('a * 'a) set @@ -178,8 +178,8 @@ generic mult_2 and mult_2_right instead. INCOMPATIBILITY. * More default pred/set conversions on a couple of relation operations -and predicates. Added powers of predicate relations. -Consolidation of some relation theorems: +and predicates. Added powers of predicate relations. Consolidation +of some relation theorems: converse_def ~> converse_unfold rel_comp_def ~> rel_comp_unfold @@ -190,8 +190,8 @@ Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. -See theory "Relation" for examples for making use of pred/set conversions -by means of attributes "to_set" and "to_pred". +See theory "Relation" for examples for making use of pred/set +conversions by means of attributes "to_set" and "to_pred". INCOMPATIBILITY. @@ -229,9 +229,9 @@ listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" -and "List.foldl plus 0", prefer "List.listsum". Otherwise it can -be useful to boil down "List.foldr" and "List.foldl" to "List.fold" -by unfolding "foldr_conv_fold" and "foldl_conv_fold". +and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be +useful to boil down "List.foldr" and "List.foldl" to "List.fold" by +unfolding "foldr_conv_fold" and "foldl_conv_fold". * Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, @@ -265,7 +265,7 @@ INCOMPATIBILITY. * Renamed facts about the power operation on relations, i.e., relpow - to match the constant's name: +to match the constant's name: rel_pow_1 ~> relpow_1 rel_pow_0_I ~> relpow_0_I @@ -295,11 +295,14 @@ INCOMPATIBILITY. * Theory Relation: Consolidated constant name for relation composition - and corresponding theorem names: +and corresponding theorem names: + - Renamed constant rel_comp to relcomp + - Dropped abbreviation pred_comp. Use relcompp instead. + - Renamed theorems: - Relation: + rel_compI ~> relcompI rel_compEpair ~> relcompEpair rel_compE ~> relcompE @@ -323,25 +326,26 @@ pred_comp_distrib ~> relcompp_distrib pred_comp_distrib2 ~> relcompp_distrib2 converse_pred_comp ~> converse_relcompp - Transitive_Closure: + finite_rel_comp ~> finite_relcomp - List: + set_rel_comp ~> set_relcomp INCOMPATIBILITY. -* New theory HOL/Library/DAList provides an abstract type for association - lists with distinct keys. +* 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. -* Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is -now inside the type class' local context. Names of affected operations and lemmas -have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with -raw red-black trees, adapt the names as follows: +* Theory HOL/Library/RBT_Impl: Backing implementation of red-black +trees is now inside a type class context. Names of affected +operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for +theories working directly with raw red-black trees, adapt the names as +follows: Operations: bulkload -> rbt_bulkload @@ -554,38 +558,45 @@ produces a rule which can be used to perform case distinction on both a list and a nat. -* Improved code generation of multisets. - -* New diagnostic command find_unused_assms to find potentially superfluous - assumptions in theorems using Quickcheck. +* Theory Library/Multiset: Improved code generation of multisets. + +* New diagnostic command 'find_unused_assms' to find potentially +superfluous assumptions in theorems using Quickcheck. * Quickcheck: + - Quickcheck returns variable assignments as counterexamples, which allows to reveal the underspecification of functions under test. For example, refuting "hd xs = x", it presents the variable assignment xs = [] and x = a1 as a counterexample, assuming that any property is false whenever "hd []" occurs in it. + These counterexample are marked as potentially spurious, as Quickcheck also returns "xs = []" as a counterexample to the obvious theorem "hd xs = hd xs". + After finding a potentially spurious counterexample, Quickcheck continues searching for genuine ones. + By default, Quickcheck shows potentially spurious and genuine - counterexamples. The option "genuine_only" sets quickcheck to - only show genuine counterexamples. + counterexamples. The option "genuine_only" sets quickcheck to only + show genuine counterexamples. - The command 'quickcheck_generator' creates random and exhaustive value generators for a given type and operations. + It generates values by using the operations as if they were constructors of that type. - Support for multisets. - Added "use_subtype" options. + - 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'. @@ -605,10 +616,10 @@ - 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. * HOL/TPTP: support to parse and import TPTP problems (all languages) - into Isabelle/HOL. +into Isabelle/HOL. *** FOL *** @@ -676,6 +687,9 @@ *** System *** +* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar +(not just JRE). + * ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name notation, which is useful for the jEdit file browser, for example.