<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Larry,<div><br></div><div>According to "hg annotate", I'm the guilty party here. I think the idea was that these lemmas were indeed already derived ad hoc and I wanted to avoid duplicates -- and probably I was too lazy or not courageous enough to get rid of the ad hoc versions and enforce the new versions throughout. By all means, if you or anybody else wants to refactor this, go ahead.</div><div><br></div><div>Best,</div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9341<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 18. Dec 2024, at 22:53, Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de> wrote:</div><br class="Apple-interchange-newline"><div><div>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?<br><br>hide_const (open) Nat.pred ― ‹hide everything related to the selector›<br>hide_fact<br> nat.case_eq_if<br> nat.collapse<br> nat.expand<br> nat.sel<br> nat.exhaust_sel<br> nat.split_sel<br> nat.split_sel_asm<br><br>Larry<br><br></div></div></blockquote></div><br></div></body></html>