src/HOL/List.thy
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.
2010-04-22 haftmann 2010-04-22 lemmas concerning remdups
2010-04-19 haftmann 2010-04-19 merged
2010-04-19 haftmann 2010-04-19 more convenient equations for zip
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-15 Cezary Kaliszyk 2010-04-15 Respectfullness and preservation of list_rel
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2010-03-17 blanchet 2010-03-17 renamed "ATP_Linkup" theory to "Sledgehammer"
2010-03-06 haftmann 2010-03-06 added insort_insert
2010-03-05 haftmann 2010-03-05 moved lemma map_sorted_distinct_set_unique
2010-03-02 paulson 2010-03-02 Slightly generalised a theorem
2010-02-22 haftmann 2010-02-22 merged
2010-02-20 haftmann 2010-02-20 lemma distinct_insert
2010-02-22 haftmann 2010-02-22 merged