# HG changeset patch
# User wenzelm
# Date 931539485 -7200
# Node ID 18c0457efd3d74c572d818828a2c1d1bbf8abf04
# Parent  9e2d97ef55d2bf1fb2ec963c62af0c62a96a2e57
mono: AddXI/Es;

diff -r 9e2d97ef55d2 -r 18c0457efd3d 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";