src/HOL/Tools/typedef_package.ML
changeset 20462 0cb88ed29776
parent 20357 5fb92bd3aaea
child 20483 04aa552a83bc
equal deleted inserted replaced
20461:d689ad772b2c 20462:0cb88ed29776
    22   val typedef: (bool * string) * (bstring * string list * mixfix) * string
    22   val typedef: (bool * string) * (bstring * string list * mixfix) * string
    23     * (string * string) option -> theory -> Proof.state
    23     * (string * string) option -> theory -> Proof.state
    24   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    24   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    25     * (string * string) option -> theory -> Proof.state
    25     * (string * string) option -> theory -> Proof.state
    26   val setup: theory -> theory
    26   val setup: theory -> theory
    27   structure TypedefData: THEORY_DATA
       
    28 end;
    27 end;
    29 
    28 
    30 structure TypedefPackage: TYPEDEF_PACKAGE =
    29 structure TypedefPackage: TYPEDEF_PACKAGE =
    31 struct
    30 struct
    32 
    31