src/HOL/Wellfounded_Recursion.thy
2008-03-07 haftmann 2008-03-07 whitespace tuning
2008-02-28 wenzelm 2008-02-28 wf_trancl: structured proof; tuned proofs; removed legacy ML bindings;
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
2008-02-15 haftmann 2008-02-15 <= and < on nat no longer depend on wellfounded relations
2008-02-06 krauss 2008-02-06 lemma wf_union_compatible: "wf R ==> wf S ==> S O R <= R ==> wf (R Un S)"
2007-11-13 berghofe 2007-11-13 Removed some case_names and consumes attributes that are now no longer needed due to changes in the to_pred and to_set attributes.
2007-10-26 haftmann 2007-10-26 dropped square syntax
2007-07-11 berghofe 2007-07-11 Adapted to changes in infrastructure for converting between sets and predicates.
2007-06-14 wenzelm 2007-06-14 tuned proofs: avoid implicit prems;
2007-06-01 krauss 2007-06-01 Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-21 huffman 2007-04-21 faster proof of wf_eq_minimal
2007-03-02 haftmann 2007-03-02 now using "class"
2007-02-07 berghofe 2007-02-07 - Adapted to new inductive definition package - Predicate version of wellfoundedness
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 ***