[isabelle-dev] error in cook book ?

[Nils Jähnig]

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.


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.


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?


best regards
Nils