src/ZF/Constructible/Relative.thy
changeset 65449 c82e63b11b8b
parent 61798 27f3c10b0b50
child 67443 3abf6a722518
     1.1 --- a/src/ZF/Constructible/Relative.thy	Sun Apr 09 20:17:00 2017 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Sun Apr 09 20:44:35 2017 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  section \<open>Relativization and Absoluteness\<close>
     1.6  
     1.7 -theory Relative imports Main begin
     1.8 +theory Relative imports ZF begin
     1.9  
    1.10  subsection\<open>Relativized versions of standard set-theoretic concepts\<close>
    1.11  
    1.12 @@ -593,13 +593,13 @@
    1.13  
    1.14  lemma (in M_trivial) pair_abs [simp]:
    1.15       "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
    1.16 -apply (simp add: pair_def ZF.Pair_def)
    1.17 +apply (simp add: pair_def Pair_def)
    1.18  apply (blast intro: transM)
    1.19  done
    1.20  
    1.21  lemma (in M_trivial) pair_in_M_iff [iff]:
    1.22       "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
    1.23 -by (simp add: ZF.Pair_def)
    1.24 +by (simp add: Pair_def)
    1.25  
    1.26  lemma (in M_trivial) pair_components_in_M:
    1.27       "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"