Re: [isabelle] Isabelle 2007 -> Isabelle 2009



Hi Steven,

type class instantiation where parameters must be defined now use explicitly the definition command (without the "where" clause):

instantiation float :: zero begin
definition Zero_float_def: "0 \<equiv> Float 0 0"
instance ..
end

Regards,
Andreas

Steven Obua schrieb:
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.