--- a/src/HOL/Import/Import_Setup.thy Sat Jan 18 10:59:00 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy Sat Jan 18 11:03:18 2025 +0100
@@ -11,6 +11,17 @@
begin
ML_file \<open>import_data.ML\<close>
+
+text \<open>
+ Initial type and constant maps, for types and constants that are not
+ defined, which means their definitions do not appear in the proof dump.
+\<close>
+import_type_map bool : bool
+import_type_map "fun" : "fun"
+import_type_map ind : ind
+import_const_map "=" : HOL.eq
+import_const_map "@" : Eps
+
ML_file \<open>import_rule.ML\<close>
end