isabelle: src/HOL/Real/Real.thy@6cb15c6f1d9f (annotated)

7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5588 diff changeset	1	(* Title: Real/Real.thy
7219 4e3f386c2e37 inserted Id: lines paulson parents: 7077 diff changeset	2	ID : $Id$
7077 60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5588 diff changeset	3	Author: Lawrence C. Paulson
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5588 diff changeset	4	Jacques D. Fleuriot
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5588 diff changeset	5	Copyright: 1998 University of Cambridge
60b098bb8b8a heavily revised by Jacques: coercions have alphabetic names; paulson parents: 5588 diff changeset	6	Description: Type "real" is a linear order
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	7	*)
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	9	Real = RealDef +
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	11	instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	12	instance real :: linorder (real_le_linear)
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	13
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14	end

author	wenzelm
	Tue, 24 Aug 1999 11:50:58 +0200
changeset 7333	6cb15c6f1d9f
parent 7219	4e3f386c2e37
child 7334	a90fc1e5fb19
permissions	-rw-r--r--