# HG changeset patch # User blanchet # Date 1375207157 -7200 # Node ID 126ee2abed9becb8db4111d47b6464c4344dfbdf # Parent aae782070611688e9d4378c362f6dd6a88b4abf1 removed spurious headings diff -r aae782070611 -r 126ee2abed9b src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 19:49:42 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 19:59:17 2013 +0200 @@ -106,14 +106,6 @@ * Nitpick *} -section {* Registering Bounded Natural Functors *} - -subsection {* Introductory Example *} - -subsection {* General Syntax *} - -section {* Generating Free Constructor Theorems *} - section {* Defining Datatypes *} subsection {* Introductory Examples *}