isabelle: src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy@0e8ac7db1f4d (annotated)

62480 f2e8984adef7 missing file; wenzelm parents: diff changeset	1	(* Title: HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
f2e8984adef7 missing file; wenzelm parents: diff changeset	2	Author: Jacques D. Fleuriot, University of Cambridge
f2e8984adef7 missing file; wenzelm parents: diff changeset	3	Author: Lawrence C Paulson, University of Cambridge
f2e8984adef7 missing file; wenzelm parents: diff changeset	4	Author: Brian Huffman
f2e8984adef7 missing file; wenzelm parents: diff changeset	5
f2e8984adef7 missing file; wenzelm parents: diff changeset	6	Nonstandard analysis.
f2e8984adef7 missing file; wenzelm parents: diff changeset	7	*)
f2e8984adef7 missing file; wenzelm parents: diff changeset	8
f2e8984adef7 missing file; wenzelm parents: diff changeset	9	theory Nonstandard_Analysis
f2e8984adef7 missing file; wenzelm parents: diff changeset	10	imports Hypercomplex
f2e8984adef7 missing file; wenzelm parents: diff changeset	11	begin
f2e8984adef7 missing file; wenzelm parents: diff changeset	12
64267 b9a1486e79be setsum -> sum nipkow parents: 62480 diff changeset	13	end