author | paulson |
Thu, 06 Jul 2000 15:01:52 +0200 | |
changeset 9266 | 1b917b8b1b38 |
parent 9043 | ca761fe227d8 |
child 14265 | 95b42e69436c |
permissions | -rw-r--r-- |
(* 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 and also satisfies plus_ac0: + is an AC-operator with zero *) RealOrd = RealDef + instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le) instance real :: linorder (real_le_linear) instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left) end