src/HOL/List.thy
2006-11-22 haftmann 2006-11-22 incorporated structure HOList into HOLogic
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 krauss 2006-11-07 Preparations for making "lexicographic_order" part of "fun"
2006-11-06 haftmann 2006-11-06 removed itrev as inlining theorem
2006-11-01 bulwahn 2006-11-01 added lexicographic_order tactic
2006-10-31 haftmann 2006-10-31 adapted seralizer syntax
2006-10-31 haftmann 2006-10-31 adapted to new serializer syntax
2006-10-26 krauss 2006-10-26 Added "recdef_wf" and "simp" attribute to "wf_measures"
2006-10-26 krauss 2006-10-26 Added "measures" combinator for lexicographic combinations of multiple measures.
2006-10-20 haftmann 2006-10-20 added reserved words for Haskell
2006-10-20 haftmann 2006-10-20 added normal post setup; cleaned up "execution" constants
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-09-25 haftmann 2006-09-25 refinements in codegen serializer
2006-09-19 haftmann 2006-09-19 added operational equality
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords
2006-08-30 haftmann 2006-08-30 code refinements
2006-08-21 haftmann 2006-08-21 more concise string serialization
2006-08-14 haftmann 2006-08-14 simplified code generator setup
2006-08-08 haftmann 2006-08-08 cleanup code generation for Numerals
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-25 haftmann 2006-07-25 added code generator serialization for Char
2006-07-23 haftmann 2006-07-23 added structure HOList
2006-07-21 haftmann 2006-07-21 added term_of_string function
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-07 haftmann 2006-06-07 slight code generator cleanup
2006-06-06 haftmann 2006-06-06 improved code lemmas
2006-06-05 krauss 2006-06-05 HOL/Tools/function_package: Added support for mutual recursive definitions.
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-05-09 haftmann 2006-05-09 introduced characters for code generator; some improved code lemmas for some list functions
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-04-27 nipkow 2006-04-27 added zip/take/drop lemmas
2006-04-09 nipkow 2006-04-09 Added function "splice"
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-21 wenzelm 2006-03-21 abbreviation upto, length;
2006-02-25 haftmann 2006-02-25 improved codegen bootstrap
2006-01-23 haftmann 2006-01-23 removed problematic keyword 'atom'
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-18 haftmann 2006-01-18 substantial improvement in serialization handling
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-09 paulson 2006-01-09 theorems need names
2005-12-22 nipkow 2005-12-22 new lemmas
2005-12-21 haftmann 2005-12-21 slight clean ups
2005-12-21 paulson 2005-12-21 removed or modified some instances of [iff]
2005-12-16 nipkow 2005-12-16 new lemmas
2005-12-02 krauss 2005-12-02 Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.
2005-10-31 nipkow 2005-10-31 A few new lemmas
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-19 nipkow 2005-10-19 added 2 lemmas
2005-10-17 wenzelm 2005-10-17 Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-11 nipkow 2005-10-11 added hd lemma
2005-10-05 nipkow 2005-10-05 added last in set lemma
2005-10-04 nipkow 2005-10-04 new hd/rev/last lemmas
2005-09-29 paulson 2005-09-29 simprules need names
2005-09-24 nipkow 2005-09-24 a few new filter lemmas
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-09-20 nipkow 2005-09-20 added a number of lemmas
2005-08-17 nipkow 2005-08-17 small mods to code lemmas