author | nipkow |
Mon, 29 Jan 2001 23:02:21 +0100 | |
changeset 10996 | 74e970389def |
parent 10751 | a81ea5d3dd41 |
permissions | -rw-r--r-- |
(* Title: HOL/HyperBin.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge Binary arithmetic for the hyperreals This case is reduced to that for the reals. *) HyperBin = HyperOrd + instance hypreal :: number defs hypreal_number_of_def "number_of v == hypreal_of_real (number_of v)" (*::bin=>hypreal ::bin=>real*) end