--- a/Ord.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/Ord.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -11,11 +11,11 @@
 val [prem] = goalw Ord.thy [mono_def]
     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
 by (REPEAT (ares_tac [allI, impI, prem] 1));
-val monoI = result();
+qed "monoI";
 
 val [major,minor] = goalw Ord.thy [mono_def]
     "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
 by (rtac (major RS spec RS spec RS mp) 1);
 by (rtac minor 1);
-val monoD = result();
+qed "monoD";