src/ZF/Tools/induct_tacs.ML
changeset 15705 b5edb9dcec9a
parent 15703 727ef1b8b3ee
child 16122 864fda4a4056
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:45:09 2005 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Apr 13 18:45:25 2005 +0200
     1.3 @@ -232,3 +232,4 @@
     1.4  
     1.5  val exhaust_tac = DatatypeTactics.exhaust_tac;
     1.6  val induct_tac  = DatatypeTactics.induct_tac;
     1.7 +