src/ZF/add_ind_def.ML

--- a/src/ZF/add_ind_def.ML	Fri Dec 22 10:48:59 1995 +0100
+++ b/src/ZF/add_ind_def.ML	Fri Dec 22 11:09:28 1995 +0100
@@ -60,6 +60,7 @@
   val inr_iff	: thm			(*injectivity of inr, using <->*)
   val distinct	: thm			(*distinctness of inl, inr using <->*)
   val distinct'	: thm			(*distinctness of inr, inl using <->*)
+  val free_SEs  : thm list		(*elim rules for SU, and pair_iff!*)
   end;
 
 signature ADD_INDUCTIVE_DEF =