diff -r 7e946a55ab4c -r dea6f877c225 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Mon Jan 20 23:07:04 2025 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Jan 20 23:30:06 2025 +0100
@@ -123,6 +123,17 @@
   "\<forall>P. P 0 \<and> (\<forall>n. P n \<longrightarrow> P (Suc n)) \<longrightarrow> (\<forall>n. P n)"
   by (auto intro: nat.induct)
 
+lemma num_Axiom:
+  "\<forall>(e::'A) f. \<exists>!fn. fn 0 = e \<and> (\<forall>n. fn (Suc n) = f (fn n) n)"
+  apply (intro allI)
+  subgoal for e f
+    apply (rule ex1I [where a = "Nat.rec_nat e (\<lambda>a b. f b a)"])
+     apply simp
+    apply (rule ext)
+    subgoal for fn x by (induct x) simp_all
+    done
+  done
+
 lemma [import_const NUMERAL]: "id = (\<lambda>x :: nat. x)"
   by auto
 
@@ -131,9 +142,10 @@
 lemma [import_const BIT0]:
   "bit0 = (SOME fn. fn (id 0) = id 0 \<and> (\<forall>n. fn (Suc n) = Suc (Suc (fn n))))"
   apply (auto intro!: some_equality[symmetric])
-  apply (auto simp add: fun_eq_iff)
-  apply (induct_tac x)
-  apply auto
+  subgoal for fn
+    apply (rule ext)
+    subgoal for x by (induct x) simp_all
+    done
   done
 
 definition [import_const BIT1, simp]: "bit1 = (\<lambda>x. Suc (bit0 x))"