src/HOL/List.thy
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
2011-05-14 haftmann 2011-05-14 use pointfree characterisation for fold_set locale
2011-05-09 noschinl 2011-05-09 add a lemma about commutative append to List.thy
2011-05-09 noschinl 2011-05-09 removed assumption from lemma List.take_add
2011-04-19 wenzelm 2011-04-19 eliminated Codegen.mode in favour of explicit argument;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2011-04-06 wenzelm 2011-04-06 separate structure Term_Position; dismantled remains of structure Type_Ext;
2011-03-30 wenzelm 2011-03-30 actually check list comprehension examples;
2011-03-28 wenzelm 2011-03-28 list comprehension: strip positions where the translation cannot handle them right now;
2011-03-22 wenzelm 2011-03-22 more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
2011-03-15 nipkow 2011-03-15 added lemma
2011-02-25 nipkow 2011-02-25 added simp lemma nth_Cons_pos to List
2011-02-03 wenzelm 2011-02-03 explicit is better than implicit;
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2011-01-07 bulwahn 2011-01-07 adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
2010-12-21 haftmann 2010-12-21 tuned type_lifting declarations