# HG changeset patch
# User wenzelm
# Date 933105894 -7200
# Node ID b02c6bdda05b068a851275e93829ef395f1e9e75
# Parent  0229ce6735f67a494b2a058558ad3d3fcc820122
fixed comments;

diff -r 0229ce6735f6 -r b02c6bdda05b src/HOL/mono.ML
--- a/src/HOL/mono.ML	Tue Jul 27 22:04:30 1999 +0200
+++ b/src/HOL/mono.ML	Tue Jul 27 22:04:54 1999 +0200
@@ -101,11 +101,10 @@
 by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
 qed "Int_Collect_mono";
 
-(*Used in individual datatype definitions*)
 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
                    ex_mono, Collect_mono, in_mono];
 
-(* Courtesy of Stefan Merz *)
+(* Courtesy of Stephan Merz *)
 Goalw [Least_def,mono_def]
   "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
 \  ==> (LEAST y. y : f``S) = f(LEAST x. x : S)";