Re: [isabelle] Question about numerals
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Question about numerals
- From: Lars Hupel <hupel at in.tum.de>
- Date: Fri, 16 Sep 2016 22:49:57 +0200
- In-reply-to: <98672027-CA5A-4811-84FC-E5D612F63C44@cam.ac.uk>
- References: <109F5AE2391E7443A0DD50C03498AAAE03458535@ait-pex02mbx05.win.dtu.dk> <98672027-CA5A-4811-84FC-E5D612F63C44@cam.ac.uk>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0
>> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and