2012-04-12 bulwahn 2012-04-12 merged
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-06 haftmann 2012-04-06 abandoned almost redundant *_foldr lemmas
2012-04-06 haftmann 2012-04-06 tuned
2012-04-06 haftmann 2012-04-06 no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
2012-03-26 nipkow 2012-03-26 reverted to canonical name
2012-03-26 nipkow 2012-03-26 Functions and lemmas by Christian Sternagel
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-02-27 nipkow 2012-02-27 converting "set [...]" to "{...}" in evaluation results
2012-02-25 bulwahn 2012-02-25 one general list_all2_update_cong instead of two special ones
2012-02-24 haftmann 2012-02-24 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-23 haftmann 2012-02-23 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
2012-02-16 bulwahn 2012-02-16 removing unnecessary premises in theorems of List theory
2012-02-10 Cezary Kaliszyk 2012-02-10 more specification of the quotient package in IsarRef
2012-02-08 blanchet 2012-02-08 use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-02-08 blanchet 2012-02-08 removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
2012-02-05 bulwahn 2012-02-05 adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
2012-02-05 bulwahn 2012-02-05 another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-02 bulwahn 2012-02-02 adding a minimally refined equality on sets for code generation
2012-01-31 bulwahn 2012-01-31 adding code equation for setsum
2012-01-23 huffman 2012-01-23 generalize type of List.listrel
2012-01-23 bulwahn 2012-01-23 adding code generation for some list relations
2012-01-10 berghofe 2012-01-10 pred_subset/equals_eq are now standard pred_set_conv rules
2012-01-07 haftmann 2012-01-07 massaging of code setup for sets
2012-01-07 haftmann 2012-01-07 corrected slip
2012-01-07 haftmann 2012-01-07 restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
2012-01-06 haftmann 2012-01-06 moved lemmas about List.set and set operations to List theory
2012-01-06 haftmann 2012-01-06 farewell to theory More_List
2012-01-06 wenzelm 2012-01-06 improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2012-01-06 haftmann 2012-01-06 incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
2012-01-05 wenzelm 2012-01-05 improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
2011-12-29 haftmann 2011-12-29 qualified Finite_Set.fold
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post; tuned text
2011-12-27 haftmann 2011-12-27 dropped fact whose names clash with corresponding facts on canonical fold
2011-12-24 haftmann 2011-12-24 dropped obsolete lemma member_set
2011-12-19 noschinl 2011-12-19 add lemmas
2011-12-15 wenzelm 2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-13 noschinl 2011-12-13 added lemmas
2011-12-09 huffman 2011-12-09 add induction rule for list_all2
2011-12-08 bulwahn 2011-12-08 removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
2011-12-01 hoelzl 2011-12-01 cardinality of sets of lists
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for lists
2011-10-03 bulwahn 2011-10-03 adding lemma to List library for executable equation of the (refl) transitive closure
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-13 bulwahn 2011-09-13 added lemma motivated by a more specific lemma in the AFP-KBPs theories
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-01 blanchet 2011-09-01 added two lemmas about "distinct" to help Sledgehammer
2011-08-30 bulwahn 2011-08-30 adding list_size_append (thanks to Rene Thiemann)
2011-08-30 bulwahn 2011-08-30 strengthening list_size_pointwise (thanks to Rene Thiemann)
2011-08-26 nipkow 2011-08-26 added lemma
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-06-27 krauss 2011-06-27 new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-05-20 haftmann 2011-05-20 names of fold_set locales resemble name of characteristic property more closely