On Wed, 8 Sep 2010, Christian Urban wrote:
> 1)
> i'm reading the cook book, and in chapter 6, page 135 on the bottom
> (latest draft from August 28th) , there is a piece of code including
> Simplifier.simproc_global_i, which gives an error.
>
> i went with simproc_i, this seems ok.
This is something that changed in Isabelle on 25 August. If
your Isabelle version is older, then simproc_i is what you
need to use.
One more thing: that change says explicitly "renamed
Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that
this is not the real thing".
The 'simproc_setup' command in Isar is the real thing here.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
