src/HOL/Ord.ML
author paulson
Mon Oct 07 10:28:44 1996 +0200 (1996-10-07)
changeset 2056 93c093620c28
parent 1465 5d7a7e439cec
child 2608 450c9b682a92
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
clasohm@1465
     1
(*  Title:      HOL/Ord.ML
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
The type class for ordered types
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
open Ord;
clasohm@923
    10
clasohm@923
    11
val [prem] = goalw Ord.thy [mono_def]
clasohm@923
    12
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
clasohm@923
    13
by (REPEAT (ares_tac [allI, impI, prem] 1));
clasohm@923
    14
qed "monoI";
clasohm@923
    15
clasohm@923
    16
val [major,minor] = goalw Ord.thy [mono_def]
clasohm@923
    17
    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
clasohm@923
    18
by (rtac (major RS spec RS spec RS mp) 1);
clasohm@923
    19
by (rtac minor 1);
clasohm@923
    20
qed "monoD";
clasohm@923
    21