author | wenzelm |
Wed, 10 May 2000 22:34:30 +0200 | |
changeset 8856 | 435187ffc64e |
parent 7706 | da41066983e5 |
child 10919 | 144ede948e58 |
permissions | -rw-r--r-- |
7292 | 1 |
(* Title: HOL/RealBin.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Binary arithmetic for the reals |
|
7 |
||
8 |
This case is reduced to that for the integers |
|
9 |
*) |
|
10 |
||
8856 | 11 |
RealBin = RealInt + |
7292 | 12 |
|
13 |
instance |
|
14 |
real :: number |
|
15 |
||
16 |
defs |
|
17 |
real_number_of_def |
|
18 |
"number_of v == real_of_int (number_of v)" |
|
19 |
(*::bin=>real ::bin=>int*) |
|
20 |
||
21 |
end |