isabelle: src/HOL/Nonstandard_Analysis/Hyperreal.thy@5ce4d117cea7 (annotated)

62479 716336f19aa9 clarified session; wenzelm parents: 51525 diff changeset	1	(* Title: HOL/Nonstandard_Analysis/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
51525 d3d170a2887f HOL-NSA should only import Complex_Main hoelzl parents: 35310 diff changeset	10	imports 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	paulson <lp15@cam.ac.uk>
	Tue, 11 Sep 2018 16:21:54 +0100
changeset 68975	5ce4d117cea7
parent 62479	716336f19aa9
permissions	-rw-r--r--