Re: [isabelle] Isabelle 2007 -> Isabelle 2009



On 09/29/2009 06:23 PM, Steven Obua wrote:
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 should do it.

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

see also HOL/Library/Float.thy.

cheers

chris





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