Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?

On 10 Aug 2012, at 12:40, Christoph LANGE wrote:

> So from x::real these provers will know that it is a real number and therefore an element of an ordered set?


>  I didn't know that one can simply say (rule name_of_lemma).

That is one of the core ideas in Isabelle, going right back to 1986.

Your project sounds interesting. Good luck!


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