author | paulson |
Fri, 16 Nov 2001 18:24:11 +0100 | |
changeset 12224 | 02df7cbe7d25 |
parent 10751 | a81ea5d3dd41 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title: HOL/HyperBin.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 hyperreals |
|
7 |
||
8 |
This case is reduced to that for the reals. |
|
9 |
*) |
|
10 |
||
11 |
HyperBin = HyperOrd + |
|
12 |
||
13 |
instance |
|
14 |
hypreal :: number |
|
15 |
||
16 |
defs |
|
17 |
hypreal_number_of_def |
|
18 |
"number_of v == hypreal_of_real (number_of v)" |
|
19 |
(*::bin=>hypreal ::bin=>real*) |
|
20 |
||
21 |
end |