isabelle: src/HOL/Real/RealOrd.thy@a901bafe4578 (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
7588 26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	14	constdefs
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	15	rabs :: real => real
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	16	"rabs r == if 0r<=r then r else -r"
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or paulson parents: 7334 diff changeset	17
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	18	end

author	wenzelm
	Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039	a901bafe4578
parent 7588	26384af93359
child 8838	4eaa99f0d223
permissions	-rw-r--r--