changeset 171 | 16c4ea954511 |
parent 118 | 5b96b1252cdc |
--- 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";