| changeset 12023 | d982f98e0f0d |
| parent 11990 | c1daefc08eff |
| child 12437 | 6d4e02b6dd43 |
--- a/src/HOL/Inductive.thy Sat Nov 03 01:33:33 2001 +0100 +++ b/src/HOL/Inductive.thy Sat Nov 03 01:33:54 2001 +0100 @@ -65,7 +65,7 @@ induct_rulify2 -subsubsection {* Inductive datatypes and primitive recursion *} +subsection {* Inductive datatypes and primitive recursion *} text {* Package setup. *}