src/ZF/Epsilon.thy
changeset 45602 2a858377c3d2
parent 39159 0dec18004e75
child 46751 6b94c39b7366
     1.1 --- a/src/ZF/Epsilon.thy	Sun Nov 20 17:57:09 2011 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Sun Nov 20 20:15:02 2011 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  apply (rule nat_0I [THEN UN_upper])
     1.5  done
     1.6  
     1.7 -lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
     1.8 +lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
     1.9  
    1.10  lemma Transset_eclose: "Transset(eclose(A))"
    1.11  apply (unfold eclose_def Transset_def)
    1.12 @@ -58,13 +58,13 @@
    1.13  
    1.14  (* x : eclose(A) ==> x <= eclose(A) *)
    1.15  lemmas eclose_subset =  
    1.16 -       Transset_eclose [unfolded Transset_def, THEN bspec, standard]
    1.17 +       Transset_eclose [unfolded Transset_def, THEN bspec]
    1.18  
    1.19  (* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
    1.20 -lemmas ecloseD = eclose_subset [THEN subsetD, standard]
    1.21 +lemmas ecloseD = eclose_subset [THEN subsetD]
    1.22  
    1.23  lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
    1.24 -lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
    1.25 +lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
    1.26  
    1.27  (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
    1.28     [| a: eclose(A);  !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x) 
    1.29 @@ -148,7 +148,7 @@
    1.30  by (simp add: lt_def Ord_def under_Memrel) 
    1.31  
    1.32  (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
    1.33 -lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
    1.34 +lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
    1.35  
    1.36  lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
    1.37