equal
deleted
inserted
replaced
|
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 |
1 open Ord; |
9 open Ord; |
2 |
10 |
3 val [prem] = goalw Ord.thy [mono_def] |
11 val [prem] = goalw Ord.thy [mono_def] |
4 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
12 "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)"; |
5 by (REPEAT (ares_tac [allI, impI, prem] 1)); |
13 by (REPEAT (ares_tac [allI, impI, prem] 1)); |