src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
author wenzelm
Sat, 24 Mar 2018 20:51:42 +0100
changeset 67945 984c3dc46cc0
parent 64267 b9a1486e79be
permissions -rw-r--r--
tuned output;
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