--- a/src/HOL/Wellfounded_Relations.thy Mon Apr 10 14:37:23 2006 +0200
+++ b/src/HOL/Wellfounded_Relations.thy Mon Apr 10 16:00:34 2006 +0200
@@ -116,13 +116,11 @@
apply (drule spec, erule mp, blast)
done
-
text{*Transitivity of WF combinators.*}
lemma trans_lex_prod [intro!]:
"[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
by (unfold trans_def lex_prod_def, blast)
-
subsubsection{*Wellfoundedness of proper subset on finite sets.*}
lemma wf_finite_psubset: "wf(finite_psubset)"
apply (unfold finite_psubset_def)