isabelle: src/HOL/Real/RealInt.thy@d3671b878828 (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
8856 435187ffc64e fixed theory deps; wenzelm parents: 7334 diff changeset	8	RealInt = RealOrd +
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	9
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	10	defs
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	11	(overloaded)
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	12	real_of_int_def
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	13	"real z == Abs_REAL(UN (i,j): Rep_Integ z. realrel ``
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	14	{(preal_of_prat(prat_of_pnat(pnat_of_nat i)),
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 10834 diff changeset	15	preal_of_prat(prat_of_pnat(pnat_of_nat j)))})"
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	16
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	17	end

author	ballarin
	Wed, 30 Apr 2003 10:01:35 +0200
changeset 13936	d3671b878828
parent 10919	144ede948e58
child 14269	502a7c95de73
permissions	-rw-r--r--