# HG changeset patch
# User berghofe
# Date 899232589 -7200
# Node ID 68775c0e40e70a691b730add52725a81d658860a
# Parent  f6f225a9d5a72d3475352e61472d50e8a7f32e50
Removed obsolete comments.

diff -r f6f225a9d5a7 -r 68775c0e40e7 src/HOL/mono.ML
--- 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];