isabelle: src/HOL/NSA/Hyperreal.thy@ac31940cfb69 (annotated)

28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 27468 diff changeset	1	(* Title: HOL/NSA/Hyperreal.thy
27468 0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	2	Author: Jacques Fleuriot, Cambridge University Computer Laboratory
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	3	Copyright 1998 University of Cambridge
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	4
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	5	Construction of the Hyperreals by the Ultrapower Construction
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	6	and mechanization of Nonstandard Real Analysis
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	7	*)
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	8
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	9	theory Hyperreal
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	10	imports Ln Deriv Taylor Integration HLog
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	11	begin
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	12
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	13	end

author	haftmann
	Wed, 28 Jan 2009 11:03:42 +0100
changeset 29655	ac31940cfb69
parent 28952	15a4b2cf8c34
child 35310	73806dbabe90
permissions	-rw-r--r--