Re: [isabelle] Question about numerals



>> It is used once in HOL/ex/Primrec.thy but it seems that it can be omitted.

That one yes, but there's also a non-trivial occurence in HOL, namely in
a tactic in "Semiring_Normalization". While a naive cleanup is possible
(inline the lemma in the tactic), I don't think this is a good idea.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.