Re: [isabelle] unexpected conversion from real to int



Dear Colin,

> Can anyone tell me why this happens, and whether there's a cleaner solution
> than to re-declare 'a' as real?

if you Ctrl-hover over your variables, you'll find that they are all
natural numbers. Applying the 'real' function to your variables does not
declare them as 'real'. Instead, try this:

lemma
  fixes a b c :: real
  shows "..."

Cheers
Lars




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