author | kleing |
Tue, 23 Dec 2003 06:35:41 +0100 | |
changeset 14316 | 91b897b9a2dc |
parent 13957 | 10dbf16be15f |
permissions | -rw-r--r-- |
(* Title: NSComplexBin.thy Author: Jacques D. Fleuriot Copyright: 2001 University of Edinburgh Descrition: Binary arithmetic for the nonstandard complex numbers This case is reduced to that for the complexes (hence reals). *) NSComplexBin = NSComplex + instance hcomplex :: number defs hcomplex_number_of_def "number_of v == hcomplex_of_complex (number_of v)" (*::bin=>complex ::bin=>complex*) end