src/HOL/List.ML
2005-04-11 nipkow 2005-04-11 tuned Map, renamed lex stuff in List.
2004-10-15 nipkow 2004-10-15 added and renamed
2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2002-05-08 wenzelm 2002-05-08 oops;
2002-05-07 wenzelm 2002-05-07 converted;
2002-04-29 nipkow 2002-04-29 added rev_take and rev_drop
2002-02-14 nipkow 2002-02-14 nodups -> distinct
2002-01-08 nipkow 2002-01-08 added filter_filter
2001-12-16 kleing 2001-12-16 list_all2_rev
2001-12-13 wenzelm 2001-12-13 isatool expandshort;
2001-10-22 paulson 2001-10-22 Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly.
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-05-31 oheimb 2001-05-31 added list_all2_trans
2001-05-08 paulson 2001-05-08 new takeWhile lemma
2001-04-24 paulson 2001-04-24 removal of image_Collect as a default simprule
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-12-20 paulson 2000-12-20 tidying, removing obsolete lemmas about 0=...
2000-11-03 wenzelm 2000-11-03 rev_exhaust: rulify;
2000-09-05 wenzelm 2000-09-05 removed Add_recdef_congs [map_cong] (see Main.thy);
2000-08-31 nipkow 2000-08-31 *** empty log message ***
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
2000-08-28 nipkow 2000-08-28 Removed map_compose from simpset.
2000-08-17 nipkow 2000-08-17 added map_cong to recdef
2000-07-24 wenzelm 2000-07-24 avoid referencing thy value; rename_numerals: use implicit theory context;
2000-07-14 paulson 2000-07-14 moved sublist from UNITY/AllocBase to List
2000-07-06 nipkow 2000-07-06 Deleted list_case thms no subsumed by case_tac
2000-06-29 paulson 2000-06-29 fixed proof to cope with the default of equalityCE instead of equalityE
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-01 paulson 2000-06-01 simplified the proof of nth_upt
2000-05-31 paulson 2000-05-31 added new proofs and simplified an old one
2000-05-26 paulson 2000-05-26 renamed upt_Suc, since that name is needed for its primrec rule
2000-05-23 paulson 2000-05-23 added type constraint ::nat because 0 is now overloaded
2000-04-19 paulson 2000-04-19 removal of less_SucI, le_SucI from default simpset
2000-03-13 wenzelm 2000-03-13 case_tac now subsumes both boolean and datatype cases;
2000-03-13 nipkow 2000-03-13 exhaust_tac -> cases_tac
2000-02-24 nipkow 2000-02-24 Added and renamed a lemma.
2000-02-18 paulson 2000-02-18 expandshort
2000-01-26 nipkow 2000-01-26 optimized xs[i:=x]!j lemmas.
2000-01-12 nipkow 2000-01-12 More lemmas.
2000-01-10 nipkow 2000-01-10 Forgot to "call" MicroJava in makefile. Added list_all2 to List.
1999-12-13 paulson 1999-12-13 expandshort
1999-11-11 nipkow 1999-11-11 Imported Conny's lemmas from MicroJava
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-08-18 nipkow 1999-08-18 Added take_all and drop_all to simpset.
1999-08-16 wenzelm 1999-08-16 'a list: Nil, Cons;
1999-07-19 paulson 1999-07-19 NatBin: binary arithmetic for the naturals
1999-07-18 nipkow 1999-07-18 Modifid length_tl
1999-06-17 paulson 1999-06-17 expandshort
1999-06-11 nipkow 1999-06-11 rev=rev lemma.
1999-06-10 paulson 1999-06-10 many new lemmas about take & drop, incl the famous take-lemma Ran expandshort
1999-06-07 nipkow 1999-06-07 Added lots of 'replicate' lemmas.
1999-04-20 paulson 1999-04-20 tidied
1999-04-15 nipkow 1999-04-15 Added new thms.
1999-04-01 pusch 1999-04-01 new definition for nth. added warnings, if primrec definition is deleted from simpset.
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-03-08 nipkow 1999-03-08 modified zip
1999-01-29 paulson 1999-01-29 expandshort
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases