src/ZF/Tools/induct_tacs.ML
changeset 6141 a6922171b396
parent 6112 5e4871c5136b
child 6556 daa00919502b
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:16:39 1999 +0100
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Jan 19 11:18:11 1999 +0100
     1.3 @@ -53,6 +53,7 @@
     1.4  type constructor_info =
     1.5    {big_rec_name : string,     (*name of the mutually recursive set*)
     1.6     constructors : term list,  (*the constructors, as Consts*)
     1.7 +   free_iffs    : thm list,   (*freeness simprules*)
     1.8     rec_rewrites : thm list};  (*recursor equations*)
     1.9  
    1.10  
    1.11 @@ -161,6 +162,9 @@
    1.12  	  {big_rec_name = big_rec_name,
    1.13  	   constructors = constructors,
    1.14  	      (*let primrec handle definition by cases*)
    1.15 +	   free_iffs = [],  (*thus we expect the necessary freeness rewrites
    1.16 +			      to be in the simpset already, as is the case for
    1.17 +			      Nat and disjoint sum*)
    1.18  	   rec_rewrites = (case recursor_eqns of
    1.19  			       [] => case_eqns | _ => recursor_eqns)};
    1.20