--- a/src/HOL/Product_Type_lemmas.ML Fri Feb 02 22:18:10 2001 +0100
+++ b/src/HOL/Product_Type_lemmas.ML Fri Feb 02 22:19:02 2001 +0100
@@ -178,7 +178,7 @@
by (Simp_tac 1);
qed "split_conv";
Addsimps [split_conv];
-(*bind_thm ("split", split_conv); (*for compatibility*)*)
+bind_thm ("split", split_conv); (*for compatibility*)
(*Subsumes the old split_Pair when f is the identity function*)
Goal "split (%x y. f(x,y)) = f";
@@ -580,5 +580,3 @@
Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
by (Blast_tac 1);
qed "Times_Diff_distrib1";
-
-