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