new theorems
authorpaulson
Tue Jun 18 10:51:04 2002 +0200 (2002-06-18)
changeset 13217bc5dc2392578
parent 13216 6104bd4088a2
child 13218 3732064ccbd1
new theorems
src/ZF/Epsilon.thy
src/ZF/WF.thy
     1.1 --- a/src/ZF/Epsilon.thy	Sun Jun 16 11:58:54 2002 +0200
     1.2 +++ b/src/ZF/Epsilon.thy	Tue Jun 18 10:51:04 2002 +0200
     1.3 @@ -132,6 +132,9 @@
     1.4  lemma under_Memrel: "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j"
     1.5  by (unfold Transset_def, blast)
     1.6  
     1.7 +lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
     1.8 +by (simp add: lt_def Ord_def under_Memrel) 
     1.9 +
    1.10  (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
    1.11  lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
    1.12  
     2.1 --- a/src/ZF/WF.thy	Sun Jun 16 11:58:54 2002 +0200
     2.2 +++ b/src/ZF/WF.thy	Tue Jun 18 10:51:04 2002 +0200
     2.3 @@ -66,6 +66,9 @@
     2.4  lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
     2.5  by (unfold wf_on_def wf_def, fast)
     2.6  
     2.7 +lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
     2.8 +by (simp add: wf_def, fast)
     2.9 +
    2.10  (** Introduction rules for wf_on **)
    2.11  
    2.12  lemma wf_onI: