ord.ML

HOL/Sum: rotated arguments of sum_case; added translation for case macro
HOL/Sum: now has Part primitives, moved from ex/Simult, with extra
laws from ZF/Sum

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