diff -r 5617622681d7 -r 55a02b8cdcf9 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Dec 19 08:26:04 2024 +0100
+++ b/src/HOL/Nat.thy	Thu Dec 19 17:01:40 2024 +0000
@@ -119,14 +119,6 @@
 declare nat.sel[code del]
 
 hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>
-hide_fact
-  nat.case_eq_if
-  nat.collapse
-  nat.expand
-  nat.sel
-  nat.exhaust_sel
-  nat.split_sel
-  nat.split_sel_asm
 
 lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
   "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"