isabelle: src/HOL/Hyperreal/HyperBin.thy@0b60b9e18a26 (annotated)

10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	1	(* Title: HOL/HyperBin.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	2	ID: $Id$
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	4	Copyright 1999 University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	6	Binary arithmetic for the hyperreals
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	8	This case is reduced to that for the reals.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	9	*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	10
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11	HyperBin = HyperOrd +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	12
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	13	instance
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	14	hypreal :: number
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	15
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	16	defs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	17	hypreal_number_of_def
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	18	"number_of v == hypreal_of_real (number_of v)"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	19	(::bin=>hypreal ::bin=>real)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	20
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	21	end

author	wenzelm
	Wed, 24 Jul 2002 00:11:24 +0200
changeset 13413	0b60b9e18a26
parent 10751	a81ea5d3dd41
permissions	-rw-r--r--