src/HOL/FixedPoint.thy
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-03-20 haftmann 2007-03-20 new lemmas
2007-03-16 haftmann 2007-03-16 adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
2007-03-12 wenzelm 2007-03-12 syntax: proper body priorty for derived binders;
2007-03-10 berghofe 2007-03-10 Generalized version of SUP and INF (with index set).
2007-03-09 haftmann 2007-03-09 stepping towards uniform lattice theory development in HOL
2007-03-02 haftmann 2007-03-02 now using "class"
2007-02-26 krauss 2007-02-26 Added lemma lfp_const: "lfp (%x. t) = t
2007-02-07 berghofe 2007-02-07 Introduction and elimination rules for <= on predicates are now declared properly.
2006-11-27 haftmann 2006-11-27 moved order arities for fun and bool to Fun/Orderings
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-13 haftmann 2006-11-13 added LOrder dependency
2006-11-12 nipkow 2006-11-12 image_constant_conv no longer [simp]
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-10-13 berghofe 2006-10-13 Generalized gfp and lfp to arbitrary complete lattices.
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-08-03 avigad 2005-08-03 combined Lfp and Gfp to FixedPoint