src/ZF/Constructible/L_axioms.thy
changeset 13299 3a932abf97e8
parent 13298 b4f370679c65
child 13304 43ef6c6dd906
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 16:59:54 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Jul 04 18:29:50 2002 +0200
     1.3 @@ -17,21 +17,21 @@
     1.4  
     1.5  lemma upair_ax: "upair_ax(L)"
     1.6  apply (simp add: upair_ax_def upair_def, clarify)
     1.7 -apply (rule_tac x="{x,y}" in exI)  
     1.8 -apply (simp add: doubleton_in_L) 
     1.9 +apply (rule_tac x="{x,y}" in rexI)  
    1.10 +apply (simp_all add: doubleton_in_L) 
    1.11  done
    1.12  
    1.13  lemma Union_ax: "Union_ax(L)"
    1.14  apply (simp add: Union_ax_def big_union_def, clarify)
    1.15 -apply (rule_tac x="Union(x)" in exI)  
    1.16 -apply (simp add: Union_in_L, auto) 
    1.17 +apply (rule_tac x="Union(x)" in rexI)  
    1.18 +apply (simp_all add: Union_in_L, auto) 
    1.19  apply (blast intro: transL) 
    1.20  done
    1.21  
    1.22  lemma power_ax: "power_ax(L)"
    1.23  apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    1.24 -apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)  
    1.25 -apply (simp add: LPow_in_L, auto)
    1.26 +apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)  
    1.27 +apply (simp_all add: LPow_in_L, auto)
    1.28  apply (blast intro: transL) 
    1.29  done
    1.30  
    1.31 @@ -63,8 +63,8 @@
    1.32  lemma replacement: "replacement(L,P)"
    1.33  apply (simp add: replacement_def, clarify)
    1.34  apply (frule LReplace_in_L, assumption+, clarify) 
    1.35 -apply (rule_tac x=Y in exI)   
    1.36 -apply (simp add: Replace_iff univalent_def, blast) 
    1.37 +apply (rule_tac x=Y in rexI)   
    1.38 +apply (simp_all add: Replace_iff univalent_def, blast) 
    1.39  done
    1.40  
    1.41  subsection{*Instantiation of the locale @{text M_triv_axioms}*}