# HG changeset patch
# User wenzelm
# Date 1003002180 -7200
# Node ID b9739c85dd440b03dc12d253b6573a8ea630dde7
# Parent  44034a6474e55aefcbec41d9812cf30b44966b26
tuned;

diff -r 44034a6474e5 -r b9739c85dd44 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Sat Oct 13 20:32:38 2001 +0200
+++ b/src/HOL/Typedef.thy	Sat Oct 13 21:43:00 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Typedef.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Munich
+*)
 
-Misc set-theory lemmas and HOL type definitions.
-*)
+header {* Set-theory lemmas and HOL type definitions *}
 
 theory Typedef = Set
 files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
@@ -24,7 +24,7 @@
 setup Rulify.setup
 
 
-section {* HOL type definitions *}
+subsection {* HOL type definitions *}
 
 constdefs
   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"