isabelle: src/HOL/Hyperreal/Hyperreal.thy@91b897b9a2dc (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	kleing
	Tue, 23 Dec 2003 06:35:41 +0100
changeset 14316	91b897b9a2dc
parent 13958	c1c67582c9b5
child 15131	c69542757a4d
permissions	-rw-r--r--