Ord.ML
author clasohm
Tue, 09 Nov 1993 13:30:13 +0100
changeset 15 25ec61ee621c
parent 0 7949f97df77a
child 118 5b96b1252cdc
permissions -rw-r--r--
renamed meson-test.ML to mesontest.ML, used exact theory names for use_thy

open Ord;

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();

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();