src/HOL/List.thy
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
2010-09-02 hoelzl 2010-09-02 Add filter_remove1
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-07-19 haftmann 2010-07-19 Scala: subtle difference in printing strings vs. complex mixfix syntax