src/HOL/List.thy
2003-12-23 kleing 2003-12-23 added some [intro?] and [trans] for list_all2 lemmas
2003-12-19 nipkow 2003-12-19 *** empty log message ***
2003-12-18 nipkow 2003-12-18 *** empty log message ***
2003-10-29 nipkow 2003-10-29 *** empty log message ***
2003-09-26 paulson 2003-09-26 misc tidying
2003-09-14 nipkow 2003-09-14 Added new theorems
2003-07-15 nipkow 2003-07-15 Some new thm (ex_map_conv?)
2003-07-11 oheimb 2003-07-11 added fold_red, o2l, postfix, some thms
2003-05-28 paulson 2003-05-28 new theorem
2003-05-14 nipkow 2003-05-14 *** empty log message ***
2003-04-16 nipkow 2003-04-16 Added take/dropWhile thms
2003-03-25 berghofe 2003-03-25 Re-structured some proofs in order to get rid of rule_format attribute.
2003-03-14 kleing 2003-03-14 more about list_all2
2002-11-29 nipkow 2002-11-29 added a few lemmas
2002-09-30 berghofe 2002-09-30 Adapted to new simplifier.
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