src/HOL/List.thy
2008-03-27 haftmann 2008-03-27 restructuring; explicit case names for rule list_induct2
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2008-02-26 haftmann 2008-02-26 char and nibble are finite
2008-02-26 bulwahn 2008-02-26 Added useful general lemmas from the work with the HeapMonad
2008-02-15 nipkow 2008-02-15 more lemmas
2008-01-25 haftmann 2008-01-25 dropped superfluous code theorems
2008-01-10 berghofe 2008-01-10 New interface for test data generators.
2007-12-10 haftmann 2007-12-10 swtiched ATP_Linkup and PreList in theory hierarchy
2007-12-07 haftmann 2007-12-07 instantiation target rather than legacy instance
2007-12-06 haftmann 2007-12-06 temporary code generator work arounds
2007-12-06 haftmann 2007-12-06 authentic primrec
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-05 kleing 2007-11-05 rev_nth
2007-11-05 nipkow 2007-11-05 added lemmas
2007-11-05 nipkow 2007-11-05 added lemmas
2007-10-28 wenzelm 2007-10-28 append/member: more light-weight way to declare authentic syntax; tuned proofs;
2007-10-27 krauss 2007-10-27 use "fun" for definition of "member" -> authentic syntax
2007-10-23 nipkow 2007-10-23 went back to >0
2007-10-23 paulson 2007-10-23 random tidying of proofs
2007-10-21 nipkow 2007-10-21 Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
2007-10-21 wenzelm 2007-10-21 avoid very slow metis invocation;
2007-10-20 chaieb 2007-10-20 fixed proofs
2007-10-18 haftmann 2007-10-18 tuned
2007-10-17 nipkow 2007-10-17 added sorted_list_of_set
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-08 berghofe 2007-10-08 list_codegen and char_codegen now call invoke_tycodegen to ensure that gen_... and term_of_... functions are generated as well.
2007-10-01 haftmann 2007-10-01 added some lemmas
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-25 ballarin 2007-09-25 Simplified proof due to improved integration of order_tac and simp.
2007-09-25 nipkow 2007-09-25 hide successor
2007-09-24 nipkow 2007-09-24 fixed haftmann bug
2007-09-20 haftmann 2007-09-20 fixed wrong syntax treatment in class target
2007-09-19 nipkow 2007-09-19 tuned
2007-09-19 paulson 2007-09-19 metis too slow
2007-09-19 nipkow 2007-09-19 Generalized [_.._] from nat to linear orders
2007-09-18 ballarin 2007-09-18 Simplified proofs due to transitivity reasoner setup.
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-09-18 nipkow 2007-09-18 sorting
2007-09-18 nipkow 2007-09-18 sorting
2007-09-10 nipkow 2007-09-10 added lemma
2007-09-04 nipkow 2007-09-04 tuned lemma; replaced !! by arbitrary
2007-08-29 nipkow 2007-08-29 turned list comprehension translations into ML to optimize base case
2007-08-29 chaieb 2007-08-29 removed unused theorems ; added lifting properties for foldr and foldl
2007-08-28 berghofe 2007-08-28 Changed "code" attribute of concat_map_singleton to "code unfold".
2007-08-28 nipkow 2007-08-28 added (code) lemmas for setsum and foldl
2007-08-20 nipkow 2007-08-20 Final mods for list comprehension
2007-08-20 nipkow 2007-08-20 removed allpairs - use list comprehension!
2007-08-17 nipkow 2007-08-17 removed set_concat_map and improved set_concat
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-07 haftmann 2007-08-07 new nbe implementation
2007-08-02 berghofe 2007-08-02 Repaired term_of_char.
2007-07-29 wenzelm 2007-07-29 proper simproc_setup for "list_neq";
2007-07-25 nipkow 2007-07-25 Added lemmas
2007-07-24 krauss 2007-07-24 renamed lemma "set_take_whileD" to "set_takeWhileD"
2007-07-11 berghofe 2007-07-11 Adapted to new package for inductive sets.
2007-07-03 wenzelm 2007-07-03 proper use of function_package ML files;
2007-06-24 nipkow 2007-06-24 new lemmas
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems; tuned partition proofs;
2007-06-06 nipkow 2007-06-06 tuned list comprehension, changed filter syntax from : to <-