src/HOLCF/LowerPD.thy
changeset 27267 5ebfb7f25ebb
parent 26962 c8b20f615d6c
child 27289 c49d427867aa
     1.1 --- a/src/HOLCF/LowerPD.thy	Wed Jun 18 22:32:06 2008 +0200
     1.2 +++ b/src/HOLCF/LowerPD.thy	Wed Jun 18 23:03:11 2008 +0200
     1.3 @@ -188,12 +188,7 @@
     1.4  
     1.5  lemma compact_imp_lower_principal:
     1.6    "compact xs \<Longrightarrow> \<exists>t. xs = lower_principal t"
     1.7 -apply (drule bifinite_compact_eq_approx)
     1.8 -apply (erule exE)
     1.9 -apply (erule subst)
    1.10 -apply (cut_tac n=i and xs=xs in approx_eq_lower_principal)
    1.11 -apply fast
    1.12 -done
    1.13 +by (rule lower_pd.compact_imp_principal)
    1.14  
    1.15  lemma lower_principal_induct:
    1.16    "\<lbrakk>adm P; \<And>t. P (lower_principal t)\<rbrakk> \<Longrightarrow> P xs"