src/HOL/Datatype.thy
changeset 18230 4dc1f30af6a1
parent 17876 b9c92f384109
child 18447 da548623916a
equal deleted inserted replaced
18229:e5a624483a23 18230:4dc1f30af6a1
    77 
    77 
    78 
    78 
    79 subsection {* Finishing the datatype package setup *}
    79 subsection {* Finishing the datatype package setup *}
    80 
    80 
    81 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    81 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
    82 hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    82 hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
    83 hide type node item
    83 hide (open) type node item
    84 
    84 
    85 
    85 
    86 subsection {* Further cases/induct rules for tuples *}
    86 subsection {* Further cases/induct rules for tuples *}
    87 
    87 
    88 lemma prod_cases3 [case_names fields, cases type]:
    88 lemma prod_cases3 [case_names fields, cases type]: