[isabelle] Isabelle 2007 -> Isabelle 2009



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.