src/HOL/List.thy
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2004-04-12 oheimb 2004-04-12 removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
2004-03-30 nipkow 2004-03-30 Added append_eq_append_conv2
2004-02-20 nipkow 2004-02-20 moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
2004-02-19 paulson 2004-02-19 new theorem
2004-02-16 kleing 2004-02-16 lemmas about card (set xs)
2004-01-07 kleing 2004-01-07 map_idI
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2004-01-05 nipkow 2004-01-05 *** empty log message ***
2003-12-24 kleing 2003-12-24 list_all2_nthD no good as [intro?]
2003-12-23 kleing 2003-12-23 list_all2_mono should not be [trans]
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]