src/HOL/FixedPoint.thy
2007-08-21 huffman 2007-08-21 Isar-style proof for lfp_ordinal_induct
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-07-11 berghofe 2007-07-11 top and bot are now constants.
2007-07-10 haftmann 2007-07-10 moved lfp_induct2 to Relation.thy
2007-05-30 haftmann 2007-05-30 generalized lemmas
2007-05-25 haftmann 2007-05-25 using rudimentary class target mechanism
2007-05-10 haftmann 2007-05-10 localized Sup/Inf
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
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