Added lemma lfp_const: "lfp (%x. t) = t

--- a/src/HOL/FixedPoint.thy	Fri Feb 23 08:39:28 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Mon Feb 26 15:08:37 2007 +0100
@@ -343,6 +343,9 @@
 lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
   by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
 
+lemma lfp_const: "lfp (\<lambda>x. t) = t"
+  by (rule lfp_unfold) (simp add:mono_def)
+
 subsection{*General induction rules for least fixed points*}
 
 theorem lfp_induct: