isabelle: src/HOL/Hyperreal/Hyperreal.thy@ed7bced29e1b (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
17635 9234108fdfb1 Added Taylor. berghofe parents: 15140 diff changeset	11	imports Poly Taylor 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	ballarin
	Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168	ed7bced29e1b
parent 17635	9234108fdfb1
child 22983	3314057c3b57
permissions	-rw-r--r--