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
1) so i stay with 2009-2.
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
On Wed, 8 Sep 2010, Nils Jähnig wrote:
yes, i found this trace buffer, but it is not really convenient to work
with, as it does not auto clear (i found now C-x C-w and try to use it)
and informations there (especially in the cook book) are meant to be
together with the other output. and i
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
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
