src/HOL/List.thy
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1998-09-21 oheimb 1998-09-21 re-added mem and list_all
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-12 oheimb 1998-08-12 replaced idt by pttrn in @filter
1998-08-08 nipkow 1998-08-08 List now contains some lexicographic orderings.
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-20 nipkow 1998-07-20 Added simproc list_eq.
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-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1998-02-06 nipkow 1998-02-06 Added `remdups' nodup -> nodups
1997-12-30 nipkow 1997-12-30 nth -> !
1997-11-05 wenzelm 1997-11-05 adapted typed_print_translation;
1997-11-04 oheimb 1997-11-04 added zip and nodup
1997-10-16 nipkow 1997-10-16 Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-05 nipkow 1997-08-05 Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-01 nipkow 1997-08-01 Corected bug in def of dropWhile (also present in Haskell lib!)
1997-07-09 nipkow 1997-07-09 Improved length = size translation.
1997-06-26 nipkow 1997-06-26 set_of_list -> set
1997-06-16 paulson 1997-06-16 Replacing the primrec definition of "length" by a translation to the built-in "size" function
1997-06-05 paulson 1997-06-05 Deleted the obsolete "pred_list" relation
1997-05-30 paulson 1997-05-30 Now Divides must be the parent
1997-05-26 paulson 1997-05-26 New operator "lists" for formalizing sets of lists
1997-05-23 nipkow 1997-05-23 Added `arbitrary'
1997-05-15 paulson 1997-05-15 Added pred_list for TFL
1997-03-06 pusch 1997-03-06 primrec definition for nth
1997-02-12 nipkow 1997-02-12 New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
1997-01-17 nipkow 1997-01-17 Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.
1996-12-10 wenzelm 1996-12-10 removed ambiguous symbols syntax;
1996-11-27 wenzelm 1996-11-27 added symbols syntax;
1996-08-19 paulson 1996-08-19 Renamed setOfList to set_of_list
1996-08-02 berghofe 1996-08-02 Simplified primrec definitions.
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-06-18 paulson 1996-06-18 Addition of setOfList
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1995-12-22 nipkow 1995-12-22 defined take/drop by induction over list rather than nat.
1995-11-29 clasohm 1995-11-29 removed quotes from types in consts and syntax sections
1995-11-12 nipkow 1995-11-12 added new arithmetic lemmas and the functions take and drop.
1995-06-29 lcp 1995-06-29 Added function rev and its properties length_rev, etc.
1995-03-28 clasohm 1995-03-28 changed syntax of datatype declarations (curried types for constructor parameters)
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application