Re: [isabelle] Use of simp add:
Am Freitag, den 29.08.2014, 09:57 +0200 schrieb Tobias Nipkow:
> On 29/08/2014 05:22, W. Douglas Maurer wrote:
> > I would appreciate some kind of strategy to determine what to write after simp
> > add: when proving a simple fact. This first came up for me when I was trying to
> > prove "floor (9.5::real) = (9::int)" and "ceiling (9.5::real) = (10::int)".
> For a start, simp should prove this, but unfortunately it does not. We will have
> to add the right lemmas to automate this, thanks.
These rules are now in the Isabelle repository:
This archive was generated by a fusion of
Pipermail (Mailman edition) and