src/HOL/Wellfounded_Relations.thy
2007-09-14 krauss 2007-09-14 added "<*mlex*>" which lexicographically combines a measure function with a relation
2007-02-07 berghofe 2007-02-07 Adapted to changes in Transitive_Closure theory.
2006-06-05 krauss 2006-06-05 Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". This simplifies some proofs.
2006-05-12 nipkow 2006-05-12 added lemma in_measure
2006-04-10 obua 2006-04-10 Moved stuff from Ring_and_Field to Matrix
2005-11-28 wenzelm 2005-11-28 added proof of measure_induct_rule;
2004-12-01 paulson 2004-12-01 fixed presentation
2004-12-01 kleing 2004-12-01 fixed another _
2004-11-30 paulson 2004-11-30 converted Wellfounded_Relations to Isar script
2001-12-06 wenzelm 2001-12-06 renamed Finite to Finite_Set;
2001-07-25 paulson 2001-07-25 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-02-15 oheimb 2001-02-15 moved inv_image to Relation
2001-01-31 oheimb 2001-01-31 improved theory reference in comment
2000-10-12 nipkow 2000-10-12 *** empty log message ***