isabelle: src/HOL/Nonstandard_Analysis/Hyperreal.thy@89347c0cc6a3 (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	haftmann
	Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734	89347c0cc6a3
parent 62479	716336f19aa9
permissions	-rw-r--r--