src/HOL/List.thy
2009-08-26 nipkow 2009-08-26 got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
2009-07-20 haftmann 2009-07-20 merged
2009-07-15 haftmann 2009-07-15 merged
2009-07-20 haftmann 2009-07-20 merged
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-15 nipkow 2009-07-15 Made "prime" executable
2009-07-15 nipkow 2009-07-15 made upt/upto executable on nat/int by simp
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-03 haftmann 2009-07-03 lemma foldl_apply_inv
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2009-06-11 nipkow 2009-06-11 two finiteness lemmas by Robert Himmelmann
2009-06-04 haftmann 2009-06-04 lemma about List.foldl and Finite_Set.fold
2009-06-02 hoelzl 2009-06-02 Added theorems about distinct & concat, map & replicate and concat & replicate
2009-05-27 nipkow 2009-05-27 more lemmas
2009-05-26 huffman 2009-05-26 listsum lemmas
2009-05-19 nipkow 2009-05-19 new lemma
2009-05-15 nipkow 2009-05-15 new lemma
2009-05-14 haftmann 2009-05-14 preprocessing must consider eq
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-05-08 nipkow 2009-05-08 more lemmas
2009-05-06 haftmann 2009-05-06 proper structures for list and string code generation stuff
2009-05-06 haftmann 2009-05-06 refined HOL string theories and corresponding ML fragments
2009-04-29 nipkow 2009-04-29 added listsum lemmas
2009-04-24 haftmann 2009-04-24 funpow and relpow with shared "^^" syntax
2009-04-20 haftmann 2009-04-20 power operation on functions with syntax o^; power operation on relations with syntax ^^
2009-04-17 haftmann 2009-04-17 separated funpow, relpow from power on monoids
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-02 nipkow 2009-03-02 name changes
2009-02-26 huffman 2009-02-26 revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
2009-02-23 huffman 2009-02-23 make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
2009-02-20 haftmann 2009-02-20 defensive implementation of pretty serialisation of lists and characters
2009-02-16 blanchet 2009-02-16 Added nitpick attribute, and fixed typo.
2009-02-10 huffman 2009-02-10 const_name antiquotations
2009-02-07 haftmann 2009-02-07 code theorems for nth, list_update
2009-02-07 haftmann 2009-02-07 code theorems for nth, list_update
2009-02-06 haftmann 2009-02-06 authentic syntax for List.nth
2009-02-03 haftmann 2009-02-03 dropped global Nil/Append interpretation
2009-01-26 haftmann 2009-01-26 sorted_take, sorted_drop
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-12-31 wenzelm 2008-12-31 eliminated OldTerm.add_term_free_names;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-11 ballarin 2008-12-11 Conversion of HOL-Main and ZF to new locales.
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-11-14 haftmann 2008-11-14 added length_unique operation for code generation
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-22 haftmann 2008-10-22 code identifier namings are no longer imperative
2008-10-20 nipkow 2008-10-20 added lemmas
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-09 haftmann 2008-10-09 established canonical argument order in SML code generators
2008-10-07 haftmann 2008-10-07 dropped superfluous if
2008-09-26 haftmann 2008-09-26 removed obsolete name convention "func"
2008-09-25 haftmann 2008-09-25 discontinued special treatment of op = vs. eq_class.eq
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-09-16 haftmann 2008-09-16 a sophisticated char/nibble conversion combinator
2008-09-16 haftmann 2008-09-16 explicit size of characters
2008-09-02 haftmann 2008-09-02 distributed literal code generation out of central infrastructure