src/ZF/add_ind_def.ML

   val fsplit_const : term		(*splitting operator for formulae*)
   val pair_iff	: thm			(*injectivity of pairing, using <->*)
   val split_eq	: thm			(*equality rule for split*)
   val fsplitI	: thm			(*intro rule for fsplit*)
   val fsplitD	: thm			(*destruct rule for fsplit*)
-  val fsplitE	: thm			(*elim rule for fsplit*)
+  val fsplitE	: thm			(*elim rule; apparently never used*)
   end;
 
 signature SU =			(** Description of a disjoint sum **)
   sig
   val sum	: term			(*disjoint sum operator*)