Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.
1.1 --- a/src/ZF/add_ind_def.ML Thu May 04 02:01:49 1995 +0200
1.2 +++ b/src/ZF/add_ind_def.ML Thu May 04 02:02:18 1995 +0200
1.3 @@ -45,7 +45,7 @@
1.4 val split_eq : thm (*equality rule for split*)
1.5 val fsplitI : thm (*intro rule for fsplit*)
1.6 val fsplitD : thm (*destruct rule for fsplit*)
1.7 - val fsplitE : thm (*elim rule for fsplit*)
1.8 + val fsplitE : thm (*elim rule; apparently never used*)
1.9 end;
1.10
1.11 signature SU = (** Description of a disjoint sum **)