src/HOL/Wellfounded_Relations.thy
Mon, 03 Dec 2007 16:04:14 +0100 haftmann shifted "fun" command to Wellfounded_Relations
Wed, 28 Nov 2007 09:01:34 +0100 haftmann dropped legacy ml bindings
Tue, 16 Oct 2007 23:12:45 +0200 haftmann global class syntax
Fri, 05 Oct 2007 08:38:09 +0200 nipkow added lemmas
Fri, 14 Sep 2007 22:21:46 +0200 krauss added "<*mlex*>" which lexicographically combines a measure function with a relation
Wed, 07 Feb 2007 17:26:49 +0100 berghofe Adapted to changes in Transitive_Closure theory.
Mon, 05 Jun 2006 14:22:58 +0200 krauss Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure".
Fri, 12 May 2006 11:19:41 +0200 nipkow added lemma in_measure
Mon, 10 Apr 2006 16:00:34 +0200 obua Moved stuff from Ring_and_Field to Matrix
Mon, 28 Nov 2005 10:58:40 +0100 wenzelm added proof of measure_induct_rule;
Wed, 01 Dec 2004 12:53:49 +0100 paulson fixed presentation
Wed, 01 Dec 2004 04:11:15 +0100 kleing fixed another _
Tue, 30 Nov 2004 16:27:44 +0100 paulson converted Wellfounded_Relations to Isar script
Thu, 06 Dec 2001 00:40:04 +0100 wenzelm renamed Finite to Finite_Set;
Wed, 25 Jul 2001 17:58:26 +0200 paulson Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Thu, 15 Feb 2001 16:00:40 +0100 oheimb moved inv_image to Relation
Wed, 31 Jan 2001 10:15:55 +0100 oheimb improved theory reference in comment
Thu, 12 Oct 2000 18:44:35 +0200 nipkow *** empty log message ***
less more (0) tip