[isabelle-dev] error in cook book ?
makarius at sketis.net
Fri Sep 10 16:14:59 CEST 2010
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.
More information about the isabelle-dev