Re: [isabelle] bug in Isabelle2005

On Fri, 28 Oct 2005, Jeremy Dawson wrote:

> bug = Main +
> consts
>   evens :: "nat set"
> inductive "evens"
>   intrs
>     evens_0 "0 : evens"
>     evens_next "n : id evens ==> Suc (Suc n) : evens"
>   monos id_mono
> end

There is indeed a problem with the ML code generator for 'inductive', but
the above is an old non-Isar theory, which is not really supported any

It is very easy to convert old theories to the current format;  ML proof
scripts work as before with the help of use_legacy_bindings.  Your theory
then looks like this (ignoring the fact that id_mono may not exist):

theory Scratch
imports Main

  evens :: "nat set"

inductive evens
    evens_0: "0 : evens"
    evens_next: "n : id evens ==> Suc (Suc n) : evens"
  monos id_mono

ML {* use_legacy_bindings (the_context ()) *}


Note that the above 'bug' is no longer present in the current Isabelle
development version, because the old theory format has been discontinued


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