src/HOL/List.ML
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
1999-01-09 nipkow 1999-01-09 Refined arith tactic.
1999-01-04 nipkow 1999-01-04 Shortened a proof.
1999-01-04 nipkow 1999-01-04 Version 1.0 of linear nat arithmetic.
1998-11-27 nipkow 1998-11-27 At last: linear arithmetic for nat!
1998-10-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers)
1998-10-14 nipkow 1998-10-14 Nat: added zero_neq_conv List: added nth/update lemmas.
1998-10-13 paulson 1998-10-13 length_Suc_conv is no longer given to AddIffs
1998-09-23 paulson 1998-09-23 deleted needless parentheses
1998-09-21 oheimb 1998-09-21 re-added mem and list_all
1998-09-10 paulson 1998-09-10 in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
1998-09-09 oheimb 1998-09-09 changed constants mem and list_all to mere translations added filter_is_subset
1998-09-04 nipkow 1998-09-04 Arith: less_diff_conv List: [i..j]
1998-09-02 nipkow 1998-09-02 Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
1998-08-20 paulson 1998-08-20 tidied
1998-08-14 paulson 1998-08-14 expandshort
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-12 oheimb 1998-08-12 added length_Suc_conv, finite_set
1998-08-10 nipkow 1998-08-10 More lemmas about lex.
1998-08-08 nipkow 1998-08-08 List now contains some lexicographic orderings.
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 nipkow 1998-08-06 New lemmas in List and Lambda in IsaMakefile
1998-07-27 nipkow 1998-07-27 conversion bug in simpproc list_eq
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-20 nipkow 1998-07-20 Added simproc list_eq.