# HG changeset patch
# User wenzelm
# Date 1004748028 -3600
# Node ID 7df1d840d01dbb469774f8a286211bef12439f62
# Parent  52aa183c15bbb4fbcf06099fc50978dcb3c3f34a
tuned;

diff -r 52aa183c15bb -r 7df1d840d01d src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Sat Nov 03 01:39:17 2001 +0100
+++ b/src/HOL/Datatype.thy	Sat Nov 03 01:40:28 2001 +0100
@@ -4,11 +4,11 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Datatype package setup -- final stage *}
+header {* Final stage of datatype setup *}
 
 theory Datatype = Datatype_Universe:
 
-(*belongs to theory Datatype_Universe; hides popular names *)
+text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
 hide const Node Atom Leaf Numb Lim Funs Split Case
 hide type node item
 
@@ -22,7 +22,6 @@
 declare case_split [cases type: bool]
   -- "prefer plain propositional version"
 
-
 rep_datatype sum
   distinct Inl_not_Inr Inr_not_Inl
   inject Inl_eq Inr_eq