clarified setup name
authorhaftmann
Mon Oct 02 23:01:14 2006 +0200 (2006-10-02)
changeset 208477e8c724339e0
parent 20846 5fde744176d7
child 20848 27a09c3eca1f
clarified setup name
src/HOL/Datatype.thy
     1.1 --- a/src/HOL/Datatype.thy	Mon Oct 02 23:01:11 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Mon Oct 02 23:01:14 2006 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4  imports NatArith Sum_Type
     1.5  begin
     1.6  
     1.7 -
     1.8  typedef (Node)
     1.9    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.10      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    1.11 @@ -537,14 +536,13 @@
    1.12  subsection {* Finishing the datatype package setup *}
    1.13  
    1.14  text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    1.15 +setup "DatatypeCodegen.setup_hooks"
    1.16  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.17  hide (open) type node item
    1.18  
    1.19  
    1.20  section {* Datatypes *}
    1.21  
    1.22 -setup "DatatypeCodegen.setup2"
    1.23 -
    1.24  subsection {* Representing primitive types *}
    1.25  
    1.26  rep_datatype bool