Something weird in Nat.thy

[Lawrence Paulson]

This theory sets up type “nat” as a standard datatype. But then it hides everything. I am okay with the hide_const for pred, but some of the facts being hidden are useful and are even derived again later in an ad-hoc manner. Any ideas why?

hide_const (open) Nat.pred ― ‹hide everything related to the selector›
hide_fact
  nat.case_eq_if
  nat.collapse
  nat.expand
  nat.sel
  nat.exhaust_sel
  nat.split_sel
  nat.split_sel_asm

Larry