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

7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	1	(* Title: RealInt.thy
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	2	ID: $Id$
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	3	Author: Jacques D. Fleuriot
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	4	Copyright: 1999 University of Edinburgh
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	5	Description: Embedding the integers in the reals
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	6	*)
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	7
7334 a90fc1e5fb19 Real/Real.thy main entry point; wenzelm parents: 7292 diff changeset	8	RealInt = RealOrd + Int +
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	9
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	10	constdefs
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	11	real_of_int :: int => real
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	12	"real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	13	{(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	14	preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	15
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	16
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	17	end

author	paulson
	Wed, 08 Mar 2000 16:15:41 +0100
changeset 8354	c02e3c131eca
parent 7334	a90fc1e5fb19
child 8856	435187ffc64e
permissions	-rw-r--r--