[isabelle] Mixed decimals and Real.thy



Hello,

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?  

Thanks,

Justin S. Davis
Formal Methods Group @ UIUC





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