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:
  http://isabelle.in.tum.de/repos/isabelle/rev/cfd3cff9387b

 - Johannes





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