# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1286325122 25200
# Node ID 2949af5e6b9c3883df76d8571d90a94cf5f90321
# Parent  9023b897e67a6599531a9f0f8775dc569538a720
move lemmas to Deflation.thy

diff -r 9023b897e67a -r 2949af5e6b9c src/HOLCF/Algebraic.thy
--- 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)
diff -r 9023b897e67a -r 2949af5e6b9c src/HOLCF/Deflation.thy
--- 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 *}