src/ZF/Constructible/L_axioms.thy
changeset 13385 31df66ca0780
parent 13363 c26eeb000470
child 13418 7c0ba9dba978
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 20:25:21 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 17 15:48:54 2002 +0200
     1.3 @@ -372,6 +372,16 @@
     1.4  apply (intro FOL_reflections)  
     1.5  done
     1.6  
     1.7 +text{*Not used.  But maybe useful?*}
     1.8 +lemma Transset_sats_empty_fm_eq_0:
     1.9 +   "[| n \<in> nat; env \<in> list(A); Transset(A)|]
    1.10 +    ==> sats(A, empty_fm(n), env) <-> nth(n,env) = 0"
    1.11 +apply (simp add: empty_fm_def empty_def Transset_def, auto)
    1.12 +apply (case_tac "n < length(env)") 
    1.13 +apply (frule nth_type, assumption+, blast)  
    1.14 +apply (simp_all add: not_lt_iff_le nth_eq_0) 
    1.15 +done
    1.16 +
    1.17  
    1.18  subsubsection{*Unordered Pairs, Internalized*}
    1.19