Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/RealOrd.thy
author fleuriot
Thu, 01 Jun 2000 11:22:27 +0200
changeset 9013 9dd0274f76af
parent 8838 4eaa99f0d223
child 9043 ca761fe227d8
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories of RealBin. Some new theorems added.

(*  Title:	 Real/RealOrd.thy
    ID: 	 $Id$
    Author:      Jacques D. Fleuriot and Lawrence C. Paulson
    Copyright:   1998  University of Cambridge
    Description: Type "real" is a linear order
*)

RealOrd = RealDef +

instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
instance real :: linorder (real_le_linear)

end
isabelle