src/ZF/Tools/induct_tacs.ML
changeset 6556 daa00919502b
parent 6141 a6922171b396
child 6851 526c0b90bcef
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
    35   struct
    35   struct
    36   val name = "ZF/datatypes";
    36   val name = "ZF/datatypes";
    37   type T = datatype_info Symtab.table;
    37   type T = datatype_info Symtab.table;
    38 
    38 
    39   val empty = Symtab.empty;
    39   val empty = Symtab.empty;
       
    40   val copy = I;
    40   val prep_ext = I;
    41   val prep_ext = I;
    41   val merge: T * T -> T = Symtab.merge (K true);
    42   val merge: T * T -> T = Symtab.merge (K true);
    42 
    43 
    43   fun print sg tab =
    44   fun print sg tab =
    44     Pretty.writeln (Pretty.strs ("datatypes:" ::
    45     Pretty.writeln (Pretty.strs ("datatypes:" ::
    61 struct
    62 struct
    62   val name = "ZF/constructors"
    63   val name = "ZF/constructors"
    63   type T = constructor_info Symtab.table
    64   type T = constructor_info Symtab.table
    64 
    65 
    65   val empty = Symtab.empty
    66   val empty = Symtab.empty
       
    67   val copy = I;
    66   val prep_ext = I
    68   val prep_ext = I
    67   val merge: T * T -> T = Symtab.merge (K true)
    69   val merge: T * T -> T = Symtab.merge (K true)
    68 
    70 
    69   fun print sg tab = ()   (*nothing extra to print*)
    71   fun print sg tab = ()   (*nothing extra to print*)
    70 end;
    72 end;