isabelle: src/HOL/Hyperreal/Hyperreal.thy@89840837108e (annotated)

13958 c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	1	(* Title: HOL/Hyperreal/Hyperreal.thy
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	2	ID: $Id$
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	3	Author: Jacques Fleuriot, Cambridge University Computer Laboratory
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	4	Copyright 1998 University of Cambridge
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	5
13958 c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	6	Construction of the Hyperreals by the Ultrapower Construction
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	7	and mechanization of Nonstandard Real Analysis
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	8	*)
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	9
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex paulson parents: 12224 diff changeset	10	theory Hyperreal = Poly + MacLaurin + HLog:
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	11
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	12	end

author	paulson
	Mon, 26 Jul 2004 17:34:52 +0200
changeset 15077	89840837108e
parent 13958	c1c67582c9b5
child 15131	c69542757a4d
permissions	-rw-r--r--