[isabelle] Mixed decimals and Real.thy
The following snippet works as expected in Isabelle2005:
ML "add_path \"$ISABELLE_HOME/src/HOL/Real\"";
theory Test = Main + Real:
lemma "ALL a. a --> a" by auto;
lemma "(1::real) + (1::real) = (2::real)" by arith;
I would also like to do something like this:
lemma "(1.5::real) + (1.5::real) = (3.0::real)" by arith;
The first period raises a syntax error in Isabelle2005.
What is the correct way to specify a real constant
as a mixed decimal?
Justin S. Davis
Formal Methods Group @ UIUC
This archive was generated by a fusion of
Pipermail (Mailman edition) and