isabelle: src/HOL/Hyperreal/Hyperreal.thy@ad4d5365d9d8 (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
22983 3314057c3b57 minimize imports huffman parents: 17635 diff changeset	11	imports Ln Poly Taylor Integration 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	nipkow
	Tue, 23 Oct 2007 23:27:23 +0200
changeset 25162	ad4d5365d9d8
parent 22983	3314057c3b57
child 26121	d4fbf84a6636
permissions	-rw-r--r--