src/HOL/List.thy
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
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-11-22 bulwahn 2010-11-22 adding code equations for EX1 on finite types
2010-11-18 haftmann 2010-11-18 mapper for list type; map_pair replaces prod_fun
2010-11-17 nipkow 2010-11-17 code eqn for slice was missing; redefined splice with fun
2010-11-05 bulwahn 2010-11-05 added two lemmas about injectivity of concat to the list theory
2010-11-02 haftmann 2010-11-02 lemmas sorted_map_same, sorted_same
2010-10-28 nipkow 2010-10-28 added lemmas about listrel(1)
2010-10-27 haftmann 2010-10-27 sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
2010-10-26 haftmann 2010-10-26 include ATP in theory List -- avoid theory edge by-passing the prominent list theory
2010-10-25 haftmann 2010-10-25 dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2010-10-06 blanchet 2010-10-06 merged
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-10-04 haftmann 2010-10-04 turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-09-28 haftmann 2010-09-28 localized listsum
2010-09-27 haftmann 2010-09-27 lemma remdups_map_remdups
2010-09-22 nipkow 2010-09-22 more lists lemmas
2010-09-21 nipkow 2010-09-21 new lemma
2010-09-17 haftmann 2010-09-17 generalized lemma insort_remove1 to insort_key_remove1
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets