--- a/src/ZF/Constructible/Rank_Separation.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/ZF/Constructible/Rank_Separation.thy Tue Jan 16 09:30:00 2018 +0100
@@ -46,7 +46,7 @@
by (intro FOL_reflections function_reflections fun_plus_reflections)
lemma obase_separation:
- \<comment>\<open>part of the order type formalization\<close>
+ \<comment> \<open>part of the order type formalization\<close>
"[| L(A); L(r) |]
==> separation(L, \<lambda>a. \<exists>x[L]. \<exists>g[L]. \<exists>mx[L]. \<exists>par[L].
ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &