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 ..


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