# HG changeset patch
# User lcp
# Date 799545738 -7200
# Node ID 380e9eb40db79b021c65592e6cbb762aec4434e2
# Parent  22b256c8c9fbb0374fa88f352a3ef70104fcd412
Changed to use split instead of fsplit.  The weakening of fsplitE appears not
to affect existing proofs.

diff -r 22b256c8c9fb -r 380e9eb40db7 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Thu May 04 02:01:49 1995 +0200
+++ b/src/ZF/add_ind_def.ML	Thu May 04 02:02:18 1995 +0200
@@ -45,7 +45,7 @@
   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 **)