author | wenzelm |
Wed, 10 May 2000 22:34:30 +0200 | |
changeset 8856 | 435187ffc64e |
parent 7334 | a90fc1e5fb19 |
child 10797 | 028d22926a41 |
permissions | -rw-r--r-- |
(* Title: RealInt.thy ID: $Id$ Author: Jacques D. Fleuriot Copyright: 1999 University of Edinburgh Description: Embedding the integers in the reals *) RealInt = RealOrd + constdefs real_of_int :: int => real "real_of_int z == Abs_real(UN (i,j): Rep_Integ z. realrel ^^ {(preal_of_prat(prat_of_pnat(pnat_of_nat i)), preal_of_prat(prat_of_pnat(pnat_of_nat j)))})" end