src/ZF/Constructible/Datatype_absolute.thy
changeset 13339 0f89104dd377
parent 13306 6eebcddee32b
child 13348 374d05460db4
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 10 16:07:52 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 10 16:54:07 2002 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4       "bnd_mono(D,h) ==> (\<Union>n\<in>nat. h^n(0)) <= lfp(D,h)"
     1.5  apply (simp add: UN_subset_iff)
     1.6  apply (rule ballI)  
     1.7 -apply (induct_tac x, simp_all) 
     1.8 +apply (induct_tac n, simp_all) 
     1.9  apply (rule subset_trans [of _ "h(lfp(D,h))"])
    1.10   apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )  
    1.11  apply (erule lfp_lemma2)