[isabelle-dev] error in cook book ?

[Makarius]

On Tue, 7 Sep 2010, Nils Jähnig 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.

The deeper problem here is on page 1, where it says "The code is as far as 
possible checked against the Isabelle distribution." with footnote 1 
saying "unidentified repository version".  This means it has been compiled 
with an arbitrary version that Christian happened to have on his laptop at 
some point.

The official Isabelle distribution is Isabelle2009-2 from June 2010.  You 
should stick with that if you want to do serious work, and not just have 
the feeling to be at the cutting edge.  (Paradoxically, "recent 
development snapshots" can age much faster than official releases, so you 
can be more out-of-date with unofficial versions if you to not catch up 
every few weeks.)


> 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.

The text describes the situation of Isabelle2009, not the latest version 
of Isabelle2009-2.  (The example stems from early adoption of the then new 
FOCUS combinator by Christian and Cezary, and I have later ironed out some 
surprising effects based on their experience with it.)


> 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?

According to the sources of Isabelle2009-2, print_tac outputs on the 
"tracing" channel.  It is up to the frontend where that appears visually 
in the end.  Proof General / Emacs version 3.7.x and pre-4.x have a 
separate "*trace*" buffer for that.  It depends on the actual Emacs 
version, OS platform, user preferences etc. how that behaves in detail. 
You might have to switch to that Emacs buffer explicitly.

Did you really manage to run PGEclipse?  I have never seen it in action 
myself.


 	Makarius