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