src/ZF/Tools/induct_tacs.ML
changeset 6556 daa00919502b
parent 6141 a6922171b396
child 6851 526c0b90bcef
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:09:33 1999 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Apr 30 18:10:03 1999 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    type T = datatype_info Symtab.table;
     1.5  
     1.6    val empty = Symtab.empty;
     1.7 +  val copy = I;
     1.8    val prep_ext = I;
     1.9    val merge: T * T -> T = Symtab.merge (K true);
    1.10  
    1.11 @@ -63,6 +64,7 @@
    1.12    type T = constructor_info Symtab.table
    1.13  
    1.14    val empty = Symtab.empty
    1.15 +  val copy = I;
    1.16    val prep_ext = I
    1.17    val merge: T * T -> T = Symtab.merge (K true)
    1.18