| changeset 13319 | 23de7b3af453 |
| parent 13316 | d16629fd0f95 |
| child 13323 | 2c287f50c9f3 |
--- a/src/ZF/Constructible/Separation.thy Tue Jul 09 10:44:41 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Tue Jul 09 10:44:53 2002 +0200 @@ -349,7 +349,7 @@ done -subsection{*Separation for @{term "well_ord_iso"}*} +subsection{*Separation for a Theorem about @{term "obase"}*} lemma obase_equals_reflects: "REFLECTS[\<lambda>x. x\<in>A --> ~(\<exists>y[L]. \<exists>g[L].