src/HOL/Ord.ML

--- a/src/HOL/Ord.ML	Fri Jul 09 18:54:55 1999 +0200
+++ b/src/HOL/Ord.ML	Fri Jul 09 18:58:05 1999 +0200
@@ -17,10 +17,12 @@
     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
 by (REPEAT (ares_tac [allI, impI, prem] 1));
 qed "monoI";
+AddXIs [monoI];
 
 Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
 by (Fast_tac 1);
 qed "monoD";
+AddXDs [monoD];
 
 
 section "Orders";