isabelle: src/HOL/NSA/Hyperreal.thy@76b51cd0a37c (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	wenzelm
	Fri, 15 Aug 2008 15:50:52 +0200
changeset 27885	76b51cd0a37c
parent 27468	0783dd1dc13d
child 28952	15a4b2cf8c34
permissions	-rw-r--r--