Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML
(* Title: OrdDefs.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Some overloaded definitions.
*)
OrdDefs = Order + Prod +
(* binary / general products *)
instance
"*" :: (le, le) le
instance
fun :: (term, le) le
defs
le_prod_def "p [= q == fst p [= fst q & snd p [= snd q"
le_fun_def "f [= g == ALL x. f x [= g x"
(* duals *)
typedef
'a dual = "{x::'a. True}"
instance
dual :: (le) le
defs
le_dual_def "x [= y == Rep_dual y [= Rep_dual x"
end