src/HOL/List.thy
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
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-28 haftmann 2010-06-28 put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem
2010-06-18 haftmann 2010-06-18 merged
2010-06-18 haftmann 2010-06-18 made List.thy a join point in the theory graph
2010-06-18 nipkow 2010-06-18 tuned set_replicate lemmas
2010-06-18 nipkow 2010-06-18 merged
2010-06-18 nipkow 2010-06-18 added lemmas
2010-06-17 haftmann 2010-06-17 rev is reverse in Haskell
2010-06-14 haftmann 2010-06-14 use various predefined Haskell operations when generating code
2010-06-12 haftmann 2010-06-12 declare lexn.simps [code del]
2010-06-02 haftmann 2010-06-02 induction over non-empty lists
2010-05-26 haftmann 2010-05-26 more convenient order of code equations
2010-05-24 haftmann 2010-05-24 more lemmas
2010-05-20 haftmann 2010-05-20 turned old-style mem into an input abbreviation
2010-05-14 nipkow 2010-05-14 added listsum lemmas
2010-05-13 nipkow 2010-05-13 Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
2010-05-12 haftmann 2010-05-12 added lemmas concerning last, butlast, insort
2010-04-20 hoelzl 2010-04-20 Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.