src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
author wenzelm
Sat, 11 Mar 2017 14:18:21 +0100
changeset 65183 37f1effd6683
parent 64267 b9a1486e79be
permissions -rw-r--r--
tuned colors;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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