src/HOL/Inductive.thy
changeset 12023 d982f98e0f0d
parent 11990 c1daefc08eff
child 12437 6d4e02b6dd43
     1.1 --- a/src/HOL/Inductive.thy	Sat Nov 03 01:33:33 2001 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Sat Nov 03 01:33:54 2001 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4    induct_rulify2
     1.5  
     1.6  
     1.7 -subsubsection {* Inductive datatypes and primitive recursion *}
     1.8 +subsection {* Inductive datatypes and primitive recursion *}
     1.9  
    1.10  text {* Package setup. *}
    1.11