[isabelle-dev] error in cook book ?

[Makarius]

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