src/HOL/Nonstandard_Analysis/Hypercomplex.thy
author wenzelm
Sun, 20 Oct 2019 20:38:22 +0200
changeset 70915 bd4d37edfee4
parent 62479 716336f19aa9
permissions -rw-r--r--
clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     1
theory Hypercomplex
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     2
imports CLim Hyperreal
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     3
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     4
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     5
end