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

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
begin

consts
  evens :: "nat set"

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

ML {* use_legacy_bindings (the_context ()) *}

end


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


	Makarius





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