1(*  Title:      HOL/Types_To_Sets/Examples/Unoverload_Def.thy
2    Author:     Fabian Immler, CMU
3*)
4theory Unoverload_Def
5  imports
6    "../Types_To_Sets"
7    Complex_Main
8begin
9
10unoverload_definition closed_def
11  and compact_eq_Heine_Borel
12  and cauchy_filter_def
13  and Cauchy_uniform
14  and nhds_def
15  and complete_uniform
16  and module_def
17  and vector_space_def
18  and module_hom_axioms_def
19  and module_hom_def
20  and VS_linear: Vector_Spaces.linear_def
21  and linear_def
22
23end