[isabelle-dev] error in cook book ?

[Christian Urban]

Hi Nils,


Nils Jähnig writes:
 > Hi,
 > 
 > 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.


 > 2)
 > then there is section about FOCUS, on page 116/117, which i copy to
 > show the lines
 > 
 > lemma
 > shows "B =⇒ ∀ x. A x"
 > apply(tactic {* rtac @{thm allI} 1 *})
 > it will produce the expected goal state
 > goal (1 subgoal):
 > 1. x. B =⇒ A x <<< THIS LINE <<<
 > But if we apply the same tactic inside FOCUS we obtain
 > lemma
 > 6.2. SIMPLE TACTICS
 > 117
 > shows "B =⇒ ∀ x. A x"
 > apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *})
 > it will produce the goal state
 > goal (1 subgoal):
 > 1. x. B =⇒ A x <<< THIS LINE <<<
 > 
 > from what the text says, this should be two different goals ... so
 > either the text should be changed, or the example.

I have to investigate this, but I think, in this
passage I wanted to describe a difference that used
to be there, but has been recently removed from 
Subgoal.FOCUS.
 
 > 3)
 > And finally a question: i can't see messages, like from print_tac or
 > the examples around 1), in emacs. so i used PGeclipse. which option do
 > i have to (un)check, to see those messages in emacs?

I am not sure what happens here. Maybe you can give 
more information.

Best wishes,
Christian