src/ZF/Constructible/Formula.thy
changeset 13339 0f89104dd377
parent 13328 703de709a64b
child 13385 31df66ca0780
     1.1 --- a/src/ZF/Constructible/Formula.thy	Wed Jul 10 16:07:52 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Jul 10 16:54:07 2002 +0200
     1.3 @@ -441,7 +441,7 @@
     1.4  
     1.5  lemma empty_in_DPow: "0 \<in> DPow(A)"
     1.6  apply (simp add: DPow_def)
     1.7 -apply (rule_tac x="Nil" in bexI) 
     1.8 +apply (rule_tac x=Nil in bexI) 
     1.9   apply (rule_tac x="Neg(Equal(0,0))" in bexI) 
    1.10    apply (auto simp add: Un_least_lt_iff) 
    1.11  done
    1.12 @@ -729,7 +729,7 @@
    1.13  text{*The subset consisting of the ordinals is definable.*}
    1.14  lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
    1.15  apply (simp add: DPow_def Collect_subset) 
    1.16 -apply (rule_tac x="Nil" in bexI) 
    1.17 +apply (rule_tac x=Nil in bexI) 
    1.18   apply (rule_tac x="ordinal_fm(0)" in bexI) 
    1.19  apply (simp_all add: sats_ordinal_fm)
    1.20  done 
    1.21 @@ -927,7 +927,7 @@
    1.22  text{*Kunen's VI, 1.10 *}
    1.23  lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
    1.24  apply (simp add: Lset_succ DPow_def) 
    1.25 -apply (rule_tac x="Nil" in bexI) 
    1.26 +apply (rule_tac x=Nil in bexI) 
    1.27   apply (rule_tac x="Equal(0,0)" in bexI) 
    1.28  apply auto 
    1.29  done
    1.30 @@ -998,7 +998,7 @@
    1.31  apply (rule LsetI [OF succI1])
    1.32  apply (simp add: DPow_def) 
    1.33  apply (intro conjI, clarify) 
    1.34 -apply (rule_tac a="x" in UN_I, simp+)  
    1.35 +apply (rule_tac a=x in UN_I, simp+)  
    1.36  txt{*Now to create the formula @{term "y \<subseteq> X"} *}
    1.37  apply (rule_tac x="Cons(X,Nil)" in bexI) 
    1.38   apply (rule_tac x="subset_fm(0,1)" in bexI)