src/ZF/Epsilon.thy
changeset 13524 604d0f3622d6
parent 13387 b7464ca2ebbb
child 13615 449a70d88b38
     1.1 --- a/src/ZF/Epsilon.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4  done
     1.5  
     1.6  (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
     1.7 -lemma eclose_induct_down: 
     1.8 +lemma eclose_induct_down [consumes 1]:
     1.9      "[| a: eclose(b);                                            
    1.10          !!y.   [| y: b |] ==> P(y);                              
    1.11          !!y z. [| y: eclose(b);  P(y);  z: y |] ==> P(z)         
    1.12 @@ -108,9 +108,6 @@
    1.13  apply (blast intro: arg_subset_eclose [THEN subsetD])
    1.14  done
    1.15  
    1.16 -(*fixed up for induct method*)
    1.17 -lemmas eclose_induct_down = eclose_induct_down [consumes 1]
    1.18 -
    1.19  lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
    1.20  apply (erule equalityI [OF eclose_least arg_subset_eclose])
    1.21  apply (rule subset_refl)