author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 8856 | 435187ffc64e |
child 10919 | 144ede948e58 |
permissions | -rw-r--r-- |
(* Title: HOL/RealBin.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge Binary arithmetic for the reals This case is reduced to that for the integers *) RealBin = RealInt + instance real :: number defs real_number_of_def "number_of v == real_of_int (number_of v)" (*::bin=>real ::bin=>int*) end