diff -r 52a16cb7fefb -r acc18a5d2b1a src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 17:19:43 2002 +0200
@@ -40,7 +40,7 @@
 apply (blast intro: transL)
 done
 
-subsubsection{*For L to satisfy Replacement *}
+subsection{*For L to satisfy Replacement *}
 
 (*Can't move these to Formula unless the definition of univalent is moved
 there too!*)