diff -r abcc438e7c27 -r 1957113f0d7d src/ZF/mono.ML
--- a/src/ZF/mono.ML	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/mono.ML	Fri Aug 12 12:51:34 1994 +0200
@@ -190,3 +190,8 @@
     "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
 by (fast_tac (FOL_cs addIs [PQimp RS mp]) 1);
 val all_mono = result();
+
+(*Used in intr_elim.ML and in individual datatype definitions*)
+val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
+		   ex_mono, Collect_mono, Part_mono, in_mono];
+