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?

Correct.

>  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!

Larry






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