src/HOL/FixedPoint.thy
Tue, 10 Jul 2007 17:30:47 +0200 haftmann moved lfp_induct2 to Relation.thy
Wed, 30 May 2007 21:09:12 +0200 haftmann generalized lemmas
Fri, 25 May 2007 21:08:52 +0200 haftmann using rudimentary class target mechanism
Thu, 10 May 2007 10:21:47 +0200 haftmann localized Sup/Inf
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Tue, 20 Mar 2007 08:27:22 +0100 haftmann new lemmas
Fri, 16 Mar 2007 21:32:08 +0100 haftmann adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
Mon, 12 Mar 2007 19:23:49 +0100 wenzelm syntax: proper body priorty for derived binders;
Sat, 10 Mar 2007 16:23:28 +0100 berghofe Generalized version of SUP and INF (with index set).
Fri, 09 Mar 2007 08:45:50 +0100 haftmann stepping towards uniform lattice theory development in HOL
Fri, 02 Mar 2007 15:43:21 +0100 haftmann now using "class"
Mon, 26 Feb 2007 15:08:37 +0100 krauss Added lemma lfp_const: "lfp (%x. t) = t
Wed, 07 Feb 2007 17:59:40 +0100 berghofe Introduction and elimination rules for <= on predicates
Mon, 27 Nov 2006 13:42:39 +0100 haftmann moved order arities for fun and bool to Fun/Orderings
less more (0) -15 tip