Ord.thy

HOL/hol.thy
renamed mk_alt_ast_tr' to alt_ast_tr';
added alternative quantifier THE;
replaced Ast by Syntax;

HOL/set.thy
replaced HOL.mk_alt_ast_tr' by HOL.alt_ast_tr';

Ord = HOL +
classes
  ord < term
consts
  "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
  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)"

end