src/HOL/List.thy
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2002-08-21 paulson 2002-08-21 Frederic Blanqui's new "guard" examples
2002-08-08 wenzelm 2002-08-08 use Tactic.prove instead of prove_goalw_cterm in internal proofs!
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-07-16 wenzelm 2002-07-16 moved stuff from Main.thy; tuned;
2002-05-30 nipkow 2002-05-30 Modifications due to enhanced linear arithmetic.
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 nipkow 2002-05-13 *** empty log message ***
2002-05-13 wenzelm 2002-05-13 tuned document;
2002-05-08 nipkow 2002-05-08 new thm distinct_conv_nth
2002-05-08 wenzelm 2002-05-08 oops;
2002-05-07 wenzelm 2002-05-07 converted;
2002-02-14 nipkow 2002-02-14 nodups -> distinct
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2000-07-16 wenzelm 2000-07-16 avoid 'split';
2000-07-14 oheimb 2000-07-14 tuned syntax
2000-07-14 paulson 2000-07-14 moved sublist from UNITY/AllocBase to List
2000-05-26 paulson 2000-05-26 named the primrec clauses of upt
2000-05-25 paulson 2000-05-25 better indentation; declared function "null"
2000-05-15 berghofe 2000-05-15 Removed unnecessary primrec equations of hd and last involving arbitrary.
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-03-16 wenzelm 2000-03-16 added HOL/PreLIst.thy;
2000-01-10 nipkow 2000-01-10 Forgot to "call" MicroJava in makefile. Added list_all2 to List.
1999-11-05 paulson 1999-11-05 added foldr
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-04-01 pusch 1999-04-01 new definition for nth. added warnings, if primrec definition is deleted from simpset.
1999-03-08 nipkow 1999-03-08 modified zip
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.