src/HOL/List.thy
2006-04-09 nipkow 2006-04-09 Added function "splice"
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-21 wenzelm 2006-03-21 abbreviation upto, length;
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-18 haftmann 2006-01-18 substantial improvement in serialization handling
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-09 paulson 2006-01-09 theorems need names
2005-12-22 nipkow 2005-12-22 new lemmas
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-12-16 nipkow 2005-12-16 new lemmas
2005-12-02 krauss 2005-12-02 Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.
2005-10-31 nipkow 2005-10-31 A few new lemmas
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-19 nipkow 2005-10-19 added 2 lemmas
2005-10-17 wenzelm 2005-10-17 Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-11 nipkow 2005-10-11 added hd lemma
2005-10-05 nipkow 2005-10-05 added last in set lemma
2005-10-04 nipkow 2005-10-04 new hd/rev/last lemmas
2005-09-29 paulson 2005-09-29 simprules need names
2005-09-24 nipkow 2005-09-24 a few new filter lemmas
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-20 nipkow 2005-09-20 added a number of lemmas
2005-08-17 nipkow 2005-08-17 small mods to code lemmas
2005-08-16 nipkow 2005-08-16 added quite a few functions for code generation
2005-08-02 nipkow 2005-08-02 Added filter lemma
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-08-01 nipkow 2005-08-01 added map_filter lemmas
2005-07-12 berghofe 2005-07-12 Auxiliary functions to be used in generated code are now defined using "attach".
2005-07-01 berghofe 2005-07-01 Adapted to new interface of code generator.
2005-06-15 nipkow 2005-06-15 added lemmas
2005-04-28 kleing 2005-04-28 more on rev
2005-04-28 kleing 2005-04-28 more about list_update
2005-04-11 nipkow 2005-04-11 tuned Map, renamed lex stuff in List.
2005-04-05 paulson 2005-04-05 lexicographic order by Norbert Voelker
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-02 berghofe 2005-02-02 Replaced application of subst by simplesubst in proof of rev_induct to avoid problems with program extraction.
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2005-01-04 kleing 2005-01-04 added list_all_rev
2004-12-22 nipkow 2004-12-22 [ .. (] -> [ ..< ]
2004-12-09 nipkow 2004-12-09 First step in reorganizing Finite_Set
2004-11-22 paulson 2004-11-22 indentation
2004-11-22 nipkow 2004-11-22 added lemmas
2004-11-21 nipkow 2004-11-21 Added more lemmas
2004-11-21 nipkow 2004-11-21 added lemmas
2004-11-21 nipkow 2004-11-21 Restructured List and added "rotate"
2004-11-13 nipkow 2004-11-13 More lemmas
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-15 nipkow 2004-10-15 added and renamed
2004-10-14 nipkow 2004-10-14 Added a few lemmas
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-09-03 paulson 2004-09-03 listrel operator for lifting relations to lists
2004-09-01 paulson 2004-09-01 new functions for sets of lists
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-05 paulson 2004-08-05 some structured proofs
2004-08-04 nipkow 2004-08-04 Added a number of new thms and the new function remove1