--- 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"