isabelle: src/HOL/NSA/Hyperreal.thy@8795cd75965e (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
35310 73806dbabe90 Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration hoelzl parents: 28952 diff changeset	10	imports Ln Deriv Taylor HLog
27468 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
	Fri, 10 Dec 2010 16:10:50 +0100
changeset 41107	8795cd75965e
parent 35310	73806dbabe90
child 51525	d3d170a2887f
permissions	-rw-r--r--