diff -r b93e6b458433 -r ca1ad6660b4a src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Thu Jan 16 12:12:32 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy	Thu Jan 16 12:41:55 2025 +0100
@@ -3,7 +3,7 @@
     Author:     Alexander Krauss, QAware GmbH
 *)
 
-section \<open>Importer machinery and required theorems\<close>
+section \<open>Importer machinery\<close>
 
 theory Import_Setup
 imports Main
@@ -11,19 +11,6 @@
 begin
 
 ML_file \<open>import_data.ML\<close>
-
-lemma light_ex_imp_nonempty: "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
-  by auto
-
-lemma typedef_hol2hollight:
-  "type_definition Rep Abs (Collect P) \<Longrightarrow> Abs (Rep a) = a \<and> P r = (Rep (Abs r) = r)"
-  by (metis type_definition.Rep_inverse type_definition.Abs_inverse
-      type_definition.Rep mem_Collect_eq)
-
-lemma ext2: "(\<And>x. f x = g x) \<Longrightarrow> f = g"
-  by (rule ext)
-
 ML_file \<open>import_rule.ML\<close>
 
 end
-