--- a/src/HOL/Hyperreal/HyperBin.thy Wed Jan 28 10:41:49 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* 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