src/HOL/Wellfounded_Recursion.thy
2006-09-19 haftmann 2006-09-19 dropped error-prone code generation 2 for wfrec
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-30 haftmann 2006-08-30 fixes
2006-07-23 haftmann 2006-07-23 small improvement in serialization for wfrec
2006-07-12 haftmann 2006-07-12 adaptions in codegen
2006-06-14 haftmann 2006-06-14 slight adaption for code generator
2006-06-13 paulson 2006-06-13 new results
2006-06-03 paulson 2006-06-03 generalized wfI
2006-05-09 haftmann 2006-05-09 improved code generation for wfrec
2006-02-07 haftmann 2006-02-07 slight improvements in code generation
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2005-12-22 wenzelm 2005-12-22 wf_induct_rule: consumes 1;
2005-09-26 berghofe 2005-09-26 Renamed wf_rec to wfrec in consts_code declaration.
2005-09-17 wenzelm 2005-09-17 added code generator setup (from Main.thy);
2005-08-09 nipkow 2005-08-09 moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy
2005-05-11 nipkow 2005-05-11 Added thms by Brian Huffmann
2004-11-30 kleing 2004-11-30 blast_tac -> blast in comment (fix latex error)
2004-11-29 paulson 2004-11-29 converted to Isar script, simplifying some results
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-05-22 berghofe 2001-05-22 Inductive characterization of wfrec combinator.
2001-02-15 oheimb 2001-02-15 added wellorder axclass
2000-10-12 nipkow 2000-10-12 *** empty log message ***