added Pair_eq to pair_ss in prod.ML
removed it locally in llist.ML because preconditions of the form <a,b> =
<?x,?y>, which used to be solved by reflexivity, now rewrote to a = ?x & b =
?y, which is not solved by reflexivity.
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