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

27468 0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	1	(* Title: HOL/Hyperreal/Hyperreal.thy
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	2	ID: $Id$
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	3	Author: Jacques Fleuriot, Cambridge University Computer Laboratory
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	4	Copyright 1998 University of Cambridge
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	5
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	6	Construction of the Hyperreals by the Ultrapower Construction
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	7	and mechanization of Nonstandard Real Analysis
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
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	10	theory Hyperreal
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	11	imports Ln Deriv Taylor Integration HLog
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	12	begin
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	13
0783dd1dc13d move nonstandard analysis theories to NSA directory huffman parents: diff changeset	14	end

author	huffman
	Thu, 03 Jul 2008 17:47:22 +0200
changeset 27468	0783dd1dc13d
child 28952	15a4b2cf8c34
permissions	-rw-r--r--