--- a/src/HOLCF/Algebraic.thy Tue Oct 05 17:07:57 2010 -0700
+++ b/src/HOLCF/Algebraic.thy Tue Oct 05 17:32:02 2010 -0700
@@ -10,10 +10,6 @@
subsection {* Constructing finite deflations by iteration *}
-lemma finite_deflation_imp_deflation:
- "finite_deflation d \<Longrightarrow> deflation d"
-unfolding finite_deflation_def by simp
-
lemma le_Suc_induct:
assumes le: "i \<le> j"
assumes step: "\<And>i. P i (Suc i)"
@@ -530,9 +526,6 @@
text {* Algebraic deflations are pointed *}
-lemma finite_deflation_UU: "finite_deflation \<bottom>"
-by default simp_all
-
lemma alg_defl_minimal:
"alg_defl_principal (Abs_fin_defl \<bottom>) \<sqsubseteq> x"
apply (induct x rule: alg_defl.principal_induct, simp)
--- a/src/HOLCF/Deflation.thy Tue Oct 05 17:07:57 2010 -0700
+++ b/src/HOLCF/Deflation.thy Tue Oct 05 17:32:02 2010 -0700
@@ -152,6 +152,13 @@
end
+lemma finite_deflation_imp_deflation:
+ "finite_deflation d \<Longrightarrow> deflation d"
+unfolding finite_deflation_def by simp
+
+lemma finite_deflation_UU: "finite_deflation \<bottom>"
+by default simp_all
+
subsection {* Continuous embedding-projection pairs *}