src/HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64267 b9a1486e79be
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Nonstandard_Analysis/Nonstandard_Analysis.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge
     3     Author:     Lawrence C Paulson, University of Cambridge
     4     Author:     Brian Huffman
     5 
     6 Nonstandard analysis.
     7 *)
     8 
     9 theory Nonstandard_Analysis
    10 imports Hypercomplex
    11 begin
    12 
    13 end