# HG changeset patch
# User paulson
# Date 1024390264 -7200
# Node ID bc5dc23925785a66313b2f01954ea0df7ae5db3e
# Parent  6104bd4088a2d3215edbf931c86170787946410a
new theorems

diff -r 6104bd4088a2 -r bc5dc2392578 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Sun Jun 16 11:58:54 2002 +0200
+++ b/src/ZF/Epsilon.thy	Tue Jun 18 10:51:04 2002 +0200
@@ -132,6 +132,9 @@
 lemma under_Memrel: "[| Transset(i);  j:i |] ==> Memrel(i)-``{j} = j"
 by (unfold Transset_def, blast)
 
+lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
+by (simp add: lt_def Ord_def under_Memrel) 
+
 (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
 lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
 
diff -r 6104bd4088a2 -r bc5dc2392578 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Sun Jun 16 11:58:54 2002 +0200
+++ b/src/ZF/WF.thy	Tue Jun 18 10:51:04 2002 +0200
@@ -66,6 +66,9 @@
 lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
 by (unfold wf_on_def wf_def, fast)
 
+lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
+by (simp add: wf_def, fast)
+
 (** Introduction rules for wf_on **)
 
 lemma wf_onI: