src/HOL/Ctr_Sugar.thy
changeset 58889 5b7a9633cfa8
parent 58659 6c9821c32dd5
child 60758 d8d85a8172b5
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     4     Copyright   2012, 2013
     4     Copyright   2012, 2013
     5 
     5 
     6 Wrapping existing freely generated type's constructors.
     6 Wrapping existing freely generated type's constructors.
     7 *)
     7 *)
     8 
     8 
     9 header {* Wrapping Existing Freely Generated Type's Constructors *}
     9 section {* Wrapping Existing Freely Generated Type's Constructors *}
    10 
    10 
    11 theory Ctr_Sugar
    11 theory Ctr_Sugar
    12 imports HOL
    12 imports HOL
    13 keywords
    13 keywords
    14   "print_case_translations" :: diag and
    14   "print_case_translations" :: diag and