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 _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev