src/HOL/List.thy
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
2008-09-01 nipkow 2008-09-01 It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
2008-09-01 nipkow 2008-09-01 cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong
2008-09-01 haftmann 2008-09-01 restructured code generation of literals
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-08-01 nipkow 2008-08-01 made setsum executable on int.
2008-07-29 nipkow 2008-07-29 added removeAll
2008-06-28 wenzelm 2008-06-28 @{lemma}: 'by' keyword;
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-05-12 krauss 2008-05-12 Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.
2008-05-07 berghofe 2008-05-07 - Explicitely applied predicate1I in a few proofs, because it is no longer part of the claset - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set attribute, because it is no longer applied automatically
2008-05-02 nipkow 2008-05-02 Added documentation