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