src/HOL/List.thy
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
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