src/HOL/ex/NormalForm.thy
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-29 haftmann 2008-10-29 adapted to strict pattern discipline
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-09-30 haftmann 2008-09-30 tuned
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-09-23 haftmann 2008-09-23 case default fallback for NBE
2008-09-05 haftmann 2008-09-05 different bookkeeping for code equations
2008-04-22 haftmann 2008-04-22 different handling of eq class for nbe
2008-04-04 haftmann 2008-04-04 postprocessing of equality
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-01-21 haftmann 2008-01-21 more lemmas
2008-01-08 haftmann 2008-01-08 normalization conversion
2007-10-25 haftmann 2007-10-25 more computation with rationals
2007-10-24 haftmann 2007-10-24 example with rational numbers
2007-10-19 haftmann 2007-10-19 added examples
2007-06-15 nipkow 2007-06-15 Church numerals added
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-03-02 haftmann 2007-03-02 tuned code theorems for ord on integers
2007-01-04 haftmann 2007-01-04 more term examples
2006-11-22 haftmann 2006-11-22 example tuned
2006-11-06 haftmann 2006-11-06 (adjustions)
2006-11-03 haftmann 2006-11-03 some example tweaking
2006-10-31 haftmann 2006-10-31 *** empty log message ***
2006-10-20 haftmann 2006-10-20 added if_delayed
2006-10-16 haftmann 2006-10-16 moved HOL code generator setup to Code_Generator
2006-10-09 nipkow 2006-10-09 added nbe_post for delayed_if
2006-10-09 nipkow 2006-10-09 added delayed_if
2006-10-02 haftmann 2006-10-02 cleaned and extended
2006-10-01 wenzelm 2006-10-01 tuned;
2006-09-19 haftmann 2006-09-19 improved numeral handling for nbe
2006-09-13 krauss 2006-09-13 Major update to function package, including new syntax and the (only theoretical) ability to handle local contexts.
2006-08-08 haftmann 2006-08-08 adding code lemma now works as expected
2006-07-25 haftmann 2006-07-25 improvements for lazy code generation
2006-06-30 nipkow 2006-06-30 normal_form to lemma test
2006-06-09 nipkow 2006-06-09 renamed file