Re: [isabelle] Mixed decimals and Real.thy



> lemma "(1.5::real) + (1.5::real) = (3.0::real)" by arith;

Isabelle does not support the dot-syntax for real numbers. You have to write
something like 15/10:

lemma "15/10 + 15/10 = (3::real)";
by arith

> lemma "(1::real) * (1::real) = (1::real)"; 
> lemma "(1::real) / (1::real) = (1::real)";

Both are solved by simp.

Tobias





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