src/ZF/Constructible/L_axioms.thy
changeset 13506 acc18a5d2b1a
parent 13505 52a16cb7fefb
child 13563 7d6c9817c432
--- 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!*)