src/HOL/Tools/typedef_package.ML
changeset 15265 a1547232fedd
parent 15259 6aa593317905
child 15457 1fbd4aba46e3
equal deleted inserted replaced
15264:a881ad2e9edc 15265:a1547232fedd
    55   val name = "HOL/typedef";
    55   val name = "HOL/typedef";
    56   type T = (typ * typ * string * string) Symtab.table;
    56   type T = (typ * typ * string * string) Symtab.table;
    57   val empty = Symtab.empty;
    57   val empty = Symtab.empty;
    58   val copy = I;
    58   val copy = I;
    59   val prep_ext = I;
    59   val prep_ext = I;
    60   val merge = Symtab.merge op =;
    60   val merge : T * T -> T = Symtab.merge op =;
    61   fun print sg _ = ();
    61   fun print sg _ = ();
    62 end;
    62 end;
    63 
    63 
    64 structure TypedefData = TheoryDataFun(TypedefArgs);
    64 structure TypedefData = TheoryDataFun(TypedefArgs);
    65 
    65