Something weird in Nat.thy

[Lawrence Paulson]

I don't understand why any refactoring would be necessary. If it is a case of for example replacing nat_induct by nat.induct, sure, although explicit references are rare (38 to be precise)

Larry

> On 19 Dec 2024, at 09:15, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote:
> 
> 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.
>