isabelle: src/HOL/Real/RealOrd.thy@4eaa99f0d223 (annotated)

7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	1	(* Title: Real/RealOrd.thy
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	2	ID: $Id$
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	3	Author: Lawrence C. Paulson
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	4	Jacques D. Fleuriot
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	5	Copyright: 1998 University of Cambridge
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	6	Description: Type "real" is a linear order
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	7	*)
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	8
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	9	RealOrd = RealDef +
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	10
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	11	instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	12	instance real :: linorder (real_le_linear)
a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	13
8838 4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 7588 diff changeset	14	defs
4eaa99f0d223 replaced rabs by overloaded abs; wenzelm parents: 7588 diff changeset	15	abs_real_def "abs r == (if 0r <= r then r else -r)"
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	16
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	17	end

author	wenzelm
	Mon, 08 May 2000 20:57:02 +0200
changeset 8838	4eaa99f0d223
parent 7588	26384af93359
child 9013	9dd0274f76af
permissions	-rw-r--r--