(* Author: René Thiemann License: LGPL *) subsection ‹Compare Instance for Rational Numbers› theory Compare_Rat imports Compare_Generator HOL.Rat begin derive (linorder) compare_order rat end