src/HOL/List.thy
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 <-
2007-06-05 chaieb 2007-06-05 added a function partition and a few lemmas
2007-06-05 chaieb 2007-06-05 added a few theorems about foldl and set
2007-06-04 nipkow 2007-06-04 tuned list comprehension
2007-06-04 haftmann 2007-06-04 authentic syntax for List.append
2007-06-03 wenzelm 2007-06-03 renamed gen_submultiset to submultiset;
2007-06-03 nipkow 2007-06-03 tuned list comprehension, added lemma
2007-06-03 nipkow 2007-06-03 *** empty log message ***
2007-06-01 nipkow 2007-06-01 Moved list comprehension into List
2007-05-24 nipkow 2007-05-24 *** empty log message ***
2007-05-21 haftmann 2007-05-21 improved code for rev
2007-05-19 haftmann 2007-05-19 constant op @ now named append
2007-05-17 haftmann 2007-05-17 abstract size function in hologic.ML
2007-05-11 nipkow 2007-05-11 *** empty log message ***
2007-05-06 haftmann 2007-05-06 PreList imports RecDef
2007-05-02 nipkow 2007-05-02 tuned allpairs
2007-04-30 nipkow 2007-04-30 added allpairs
2007-04-26 haftmann 2007-04-26 moved code generation pretty integers and characters to separate theories
2007-04-25 nipkow 2007-04-25 new lemma splice_length
2007-04-11 haftmann 2007-04-11 tuned
2007-03-30 haftmann 2007-03-30 paraphrasing equality
2007-03-28 berghofe 2007-03-28 Improved code generator for characters: now handles non-printable characters as well.
2007-03-23 haftmann 2007-03-23 two further properties about lists
2007-03-21 krauss 2007-03-21 added another rule for simultaneous induction, and lemmas for zip
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2007-01-21 nipkow 2007-01-21 Added simproc list_neq (prompted by an application)
2006-12-27 haftmann 2006-12-27 added OCaml code generation (without dictionaries)
2006-12-21 haftmann 2006-12-21 added code lemmas for quantification over bounded nats