src/ZF/Constructible/Rank.thy

--- a/src/ZF/Constructible/Rank.thy	Mon Oct 14 10:44:32 2002 +0200
+++ b/src/ZF/Constructible/Rank.thy	Mon Oct 14 11:32:00 2002 +0200
@@ -666,6 +666,12 @@
 
 
 
+subsection {*Absoluteness of Well-Founded Relations*}
+
+text{*Relativized to @{term M}: Every well-founded relation is a subset of some
+inverse image of an ordinal.  Key step is the construction (in @{term M}) of a
+rank function.*}
+
 locale M_wfrank = M_trancl +
   assumes wfrank_separation:
      "M(r) ==>