author | lcp |
Thu, 21 Apr 1994 11:28:32 +0200 | |
changeset 68 | acad709cad5d |
parent 0 | 7949f97df77a |
permissions | -rw-r--r-- |
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();