src/ZF/add_ind_def.ML
changeset 1109 380e9eb40db7
parent 750 019aadf0e315
child 1418 f5f97ee67cbb
--- 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 **)