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
     1 (*  Title:      HOL/Ord.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The type class for ordered types
     7 *)
     8 
     9 open Ord;
    10 
    11 val [prem] = goalw Ord.thy [mono_def]
    12     "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
    13 by (REPEAT (ares_tac [allI, impI, prem] 1));
    14 qed "monoI";
    15 
    16 val [major,minor] = goalw Ord.thy [mono_def]
    17     "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
    18 by (rtac (major RS spec RS spec RS mp) 1);
    19 by (rtac minor 1);
    20 qed "monoD";
    21