src/ZF/Constructible/L_axioms.thy
changeset 13506 acc18a5d2b1a
parent 13505 52a16cb7fefb
child 13563 7d6c9817c432
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 17:19:43 2002 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  apply (blast intro: transL)
     1.5  done
     1.6  
     1.7 -subsubsection{*For L to satisfy Replacement *}
     1.8 +subsection{*For L to satisfy Replacement *}
     1.9  
    1.10  (*Can't move these to Formula unless the definition of univalent is moved
    1.11  there too!*)