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

5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	1	(* Title: Real/Real.thy
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	2	ID: $Id$
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	4	Copyright 1998 University of Cambridge
5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5
5588 a3ab526bb891 Revised version with Abelian group simprocs paulson parents: 5078 diff changeset	6	Type "real" is a linear order
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
	Fri, 16 Jul 1999 22:25:07 +0200
changeset 7025	afbd8241797b
parent 5588	a3ab526bb891
child 7077	60b098bb8b8a
permissions	-rw-r--r--