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

9013 9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	1	(* Title: Real/RealOrd.thy
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	2	ID: $Id$
9dd0274f76af Updated files to remove 0r and 1r from theorems in descendant theories fleuriot parents: 8838 diff changeset	3	Author: Jacques D. Fleuriot and Lawrence C. Paulson
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	4	Copyright: 1998 University of Cambridge
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	5	Description: Type "real" is a linear order and also
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	6	satisfies plus_ac0: + is an AC-operator with zero
7334 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
9043 ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	14	instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)
ca761fe227d8 First round of changes, towards installation of simprocs paulson parents: 9013 diff changeset	15
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: diff changeset	16	end

author	nipkow
	Tue, 09 Jan 2001 15:32:27 +0100
changeset 10834	a7897aebbffc
parent 9043	ca761fe227d8
child 14265	95b42e69436c
permissions	-rw-r--r--