src/HOL/List.ML
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.
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-07-06 nipkow 1998-07-06 Converted to Auto_tac
1998-07-03 wenzelm 1998-07-03 removed duplicate thms;
1998-06-24 nipkow 1998-06-24 * HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...].
1998-06-17 nipkow 1998-06-17 goal -> Goal
1998-05-18 nipkow 1998-05-18 Cleaned up and simplified etc. snoc_induct/exhaust -> rev_induct_exhaust.
1998-05-12 nipkow 1998-05-12 Removed duplicate list_length_induct
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1998-02-24 nipkow 1998-02-24 Added some lemmas.
1998-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1998-02-12 wenzelm 1998-02-12 *** empty log message ***
1998-02-06 nipkow 1998-02-06 Added `remdups' nodup -> nodups
1997-12-30 nipkow 1997-12-30 nth -> !
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-04 oheimb 1997-11-04 added zip and nodup
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 expand_list_case -> split_list_case
1997-10-30 nipkow 1997-10-30 For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).