isabelle: src/HOL/Real/RealBin.thy@56610e2ba220 (annotated)

7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	1	(* Title: HOL/RealBin.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: Lawrence C Paulson, Cambridge University Computer Laboratory
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	4	Copyright 1999 University of Cambridge
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	5
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	6	Binary arithmetic for the reals
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	7
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	8	This case is reduced to that for the integers
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	9	*)
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	10
8856 435187ffc64e fixed theory deps; wenzelm parents: 7706 diff changeset	11	RealBin = RealInt +
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	12
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	13	instance
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	14	real :: number
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	15
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	16	defs
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	17	real_number_of_def
10919 144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 8856 diff changeset	18	"number_of v == real (number_of v :: int)"
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real paulson parents: 8856 diff changeset	19	(::bin=>real ::bin=>int)
7292 dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	20
dff3470c5c62 real literals using binary arithmetic paulson parents: diff changeset	21	end

author	wenzelm
	Tue, 06 Aug 2002 11:22:05 +0200
changeset 13462	56610e2ba220
parent 10919	144ede948e58
child 14365	3d4df8c166ae
permissions	-rw-r--r--