src/HOL/Datatype.thy
changeset 12029 7df1d840d01d
parent 11954 3d1780208bf3
child 12918 bca45be2d25b
     1.1 --- a/src/HOL/Datatype.thy	Sat Nov 03 01:39:17 2001 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sat Nov 03 01:40:28 2001 +0100
     1.3 @@ -4,11 +4,11 @@
     1.4      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.5  *)
     1.6  
     1.7 -header {* Datatype package setup -- final stage *}
     1.8 +header {* Final stage of datatype setup *}
     1.9  
    1.10  theory Datatype = Datatype_Universe:
    1.11  
    1.12 -(*belongs to theory Datatype_Universe; hides popular names *)
    1.13 +text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    1.14  hide const Node Atom Leaf Numb Lim Funs Split Case
    1.15  hide type node item
    1.16  
    1.17 @@ -22,7 +22,6 @@
    1.18  declare case_split [cases type: bool]
    1.19    -- "prefer plain propositional version"
    1.20  
    1.21 -
    1.22  rep_datatype sum
    1.23    distinct Inl_not_Inr Inr_not_Inl
    1.24    inject Inl_eq Inr_eq