diff -r 6254f50e5ec9 -r a9f7ff3a464c Ord.thy --- a/Ord.thy Fri Sep 16 15:48:20 1994 +0200 +++ b/Ord.thy Wed Sep 21 15:40:41 1994 +0200 @@ -1,23 +1,25 @@ -(* Title: HOL/Ord.thy +(* Title: HOL/Ord.thy ID: $Id$ - Author: Tobias Nipkow, Cambridge University Computer Laboratory + Author: Tobias Nipkow, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -The type class for ordered types +The type class for ordered types (* FIXME improve comment *) *) Ord = HOL + -classes + +axclass ord < term + consts "<", "<=" :: "['a::ord, 'a] => bool" (infixl 50) - mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) - min,max :: "['a::ord,'a] => 'a" + mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) + min, max :: "['a::ord, 'a] => 'a" -rules - -mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" -min_def "min(a,b) == if(a <= b, a, b)" -max_def "max(a,b) == if(a <= b, b, a)" +defs + mono_def "mono(f) == (!A B. A <= B --> f(A) <= f(B))" + min_def "min(a, b) == if(a <= b, a, b)" + max_def "max(a, b) == if(a <= b, b, a)" end +