isabelle: src/HOL/Hyperreal/Hyperreal.thy@04246269386e (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
15131 c69542757a4d New theory header syntax. nipkow parents: 13958 diff changeset	10	theory Hyperreal
15140 322485b816ac import -> imports nipkow parents: 15131 diff changeset	11	imports Poly MacLaurin HLog
15131 c69542757a4d New theory header syntax. nipkow parents: 13958 diff changeset	12	begin
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	13
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: diff changeset	14	end

author	paulson
	Wed, 27 Jul 2005 11:28:18 +0200
changeset 16924	04246269386e
parent 15140	322485b816ac
child 17635	9234108fdfb1
permissions	-rw-r--r--