# HG changeset patch
# User paulson
# Date 1734627714 0
# Node ID 445d27ab591be7f6c0275a352b2eb3f86b995b4b
# Parent  362b2ff84206ea966a6c3fbc4879b52eb82cf153# Parent  55a02b8cdcf97560d4850e4ba521778261931134
merged

diff -r 362b2ff84206 -r 445d27ab591b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Dec 19 16:01:06 2024 +0100
+++ b/src/HOL/Nat.thy	Thu Dec 19 17:01:54 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"