src/HOL/BNF/BNF_GFP.thy
changeset 51782 84e7225f5ab6
parent 51739 3514b90d0a8b
child 51804 be6e703908f4
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -224,9 +224,7 @@
     1.4  unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
     1.5  
     1.6  lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
     1.7 -unfolding cpow_def clists_def
     1.8 -by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
     1.9 -   (erule notE, erule ordIso_transitive, rule czero_ordIso)
    1.10 +unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
    1.11  
    1.12  lemma incl_UNION_I:
    1.13  assumes "i \<in> I" and "A \<subseteq> F i"