# HG changeset patch
# User krauss
# Date 1172498917 -3600
# Node ID fe054a72d9ce95a12e09da45ebe2ced6a13437cf
# Parent  f9d35783d28d54e66be62267f369868f2034b3c8
Added lemma lfp_const: "lfp (%x. t) = t

diff -r f9d35783d28d -r fe054a72d9ce src/HOL/FixedPoint.thy
--- 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: