Re: [isabelle] real number calculation

> Also, how to express the pre-condition that "a is within the area [0,1]"?

You could just write "0 <= a & a <= 1". Aternatively, there is a theory of
intervals (SetInterval.thy) that provides the necessary notation, in this
case "a : {0..1}".


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