src/ZF/Constructible/Relative.thy
changeset 13535 007559e981c7
parent 13514 cc3bbaf1b8d3
child 13543 2b3c7e319d82
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Aug 27 11:09:33 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Aug 27 11:09:35 2002 +0200
     1.3 @@ -802,14 +802,6 @@
     1.4        ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
     1.5  by (simp add: is_nat_case_def) 
     1.6  
     1.7 -lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
     1.8 -     "M(Inl(a)) <-> M(a)"
     1.9 -by (simp add: Inl_def) 
    1.10 -
    1.11 -lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
    1.12 -     "M(Inr(a)) <-> M(a)"
    1.13 -by (simp add: Inr_def)
    1.14 -
    1.15  
    1.16  subsection{*Absoluteness for Ordinals*}
    1.17  text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}