Re: [isabelle] Isabelle 2007 -> Isabelle 2009



An updated version of our Floating-Point library is already available:

import "~~/src/HOL/Library/Float"

or:

instantiation float :: zero begin
definition zero_float where "0 = Float 0 0"
instance ..
end


  Johannes


Am Dienstag, den 29.09.2009, 18:23 +0200 schrieb Steven Obua:
> Hi,
> I want to convert some Isabelle 2007 stuff to Isabelle 2009. I  
> encountered problems with this:
> 
> datatype float = Float int int
> 
> instance float :: zero
>    Zero_float_def: "0 \<equiv> Float 0 0" ..
> 
> How do I write this the Isabelle 2009 way? Any quick idea?
> 
> Steven Obua






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