src/HOL/List.thy
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
2008-04-25 krauss 2008-04-25 * New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size
2008-04-22 haftmann 2008-04-22 dropped some metis calls
2008-04-09 huffman 2008-04-09 move lemmas from Word/BinBoolList.thy to List.thy
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
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