src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
author wenzelm
Tue, 01 Mar 2016 10:32:55 +0100
changeset 62480 f2e8984adef7
child 64267 b9a1486e79be
permissions -rw-r--r--
missing file;
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
f2e8984adef7 missing file;
wenzelm
parents:
diff changeset
    13
end