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