isabelle: src/HOL/NSA/Hyperreal.thy@c21f2c52f54b (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
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	blanchet
	Fri, 01 Aug 2014 15:08:49 +0200
changeset 57838	c21f2c52f54b
parent 51525	d3d170a2887f
permissions	-rw-r--r--