Removed obsolete comments.

--- a/src/HOL/mono.ML	Tue Jun 30 20:46:35 1998 +0200
+++ b/src/HOL/mono.ML	Tue Jun 30 20:49:49 1998 +0200
@@ -95,14 +95,13 @@
 by (blast_tac (claset() addIs [PQimp RS mp]) 1);
 qed "Collect_mono";
 
-(*Used in indrule.ML*)
 val [subs,PQimp] = goal Set.thy
     "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
 \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
 qed "Int_Collect_mono";
 
-(*Used in intr_elim.ML and in individual datatype definitions*)
+(*Used in individual datatype definitions*)
 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
                    ex_mono, Collect_mono, in_mono];