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

author | wenzelm |

Mon, 09 Jan 2012 14:47:18 +0100 | |

changeset 46160 | f363e5a2f8e8 |

parent 46159 | 05a82dd869ed |

child 46161 | 4ed94d92ae19 |

misc tuning and reformatting;

--- a/NEWS Mon Jan 09 14:26:13 2012 +0100 +++ b/NEWS Mon Jan 09 14:47:18 2012 +0100 @@ -41,8 +41,8 @@ * 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 +* 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" @@ -60,7 +60,21 @@ *** HOL *** -* Consolidated various theorem names relating to Finite_Set.fold combinator: +* 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. 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. + +* Consolidated various theorem names relating to Finite_Set.fold +combinator: + inf_INFI_fold_inf ~> inf_INF_fold_inf sup_SUPR_fold_sup ~> sup_SUP_fold_sup INFI_fold_inf ~> INF_fold_inf @@ -71,6 +85,7 @@ INCOMPATIBILITY. * Consolidated theorem names concerning fold combinators: + INFI_set_fold ~> INF_set_fold SUPR_set_fold ~> SUP_set_fold INF_code ~> INF_set_foldr @@ -79,15 +94,18 @@ foldl.simps ~> foldl_Nil foldl_Cons foldr_fold_rev ~> foldr_def foldl_fold ~> foldl_def + INCOMPATIBILITY. -* Dropped rarely useful theorems concerning fold combinators: foldl_apply, -foldl_fun_comm, foldl_rev, fold_weak_invariant, rev_foldl_cons, fold_set_remdups, -fold_set, fold_set1, concat_conv_foldl, foldl_weak_invariant, foldl_invariant, -foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, listsum_conv_fold, -listsum_foldl, sort_foldl_insort. INCOMPATIBILITY. Prefer "List.fold" with -canonical argument order, or boil down "List.foldr" and "List.foldl" to "List.fold" -by unfolding "foldr_def" and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0" +* Dropped rarely useful theorems concerning fold combinators: +foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant, +rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, +concat_conv_foldl, foldl_weak_invariant, foldl_invariant, +foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, +listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY. +Prefer "List.fold" with canonical argument order, or boil down +"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def" +and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0" and "List.foldl plus 0", prefer "List.listsum". * Concrete syntax for case expressions includes constraints for source @@ -101,8 +119,9 @@ * Finite_Set.fold now qualified. INCOMPATIBILITY. -* Renamed some facts on canonical fold on lists, in order to avoid problems -with interpretation involving corresponding facts on foldl with the same base names: +* Renamed some facts on canonical fold on lists, in order to avoid +problems with interpretation involving corresponding facts on foldl +with the same base names: fold_set_remdups ~> fold_set_fold_remdups fold_set ~> fold_set_fold @@ -110,26 +129,17 @@ INCOMPATIBILITY. -* 'set' is now a proper type constructor. Definitions mem_def and Collect_def -have disappeared. 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. -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 Isabelle 2011-1 before jumping to the current release. - -* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY. +* Theory HOL/Library/AList has been renamed to + AList_Impl. INCOMPATIBILITY. * 'datatype' specifications allow explicit sort constraints. -* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use -theory HOL/Library/Nat_Bijection instead. - -* Session HOL-Word: Discontinued many redundant theorems specific to type -'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. +* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, +use theory HOL/Library/Nat_Bijection instead. + +* 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