Re: [isabelle] PIDE Display of Assumptions
On Fri, 29 Jun 2012, Christian Urban wrote:
Is there a way to make that printmode the default
in ones etc/settings, for example?
Following usual Isabelle conventions, src/Tools/jEdit/etc/settings defines
various settings that are relavant for that tool. ISABELLE_JEDIT_OPTIONS
allows to give default command line options. So you can set that
accordingly somewhere in your local $ISABELLE_HOME_USER/etc/settings for
I have to admit I am very fond of this special syntax too and have no
problem with interpreting them in my head as
C F G H I
which is the style that usually appears in textbooks on
natural deduction. For example, the Gentzen book would
write the impI- and orE-rules as
A --> B
A v B C C
which is not very different from Larry's bracket notation.
That is the reason why Larry introduced that in the late 1980-ies, and why
I've spent some time in 1993 to make it print realiably.
The nesting of rules does not fit very well in that notation, though, and
it is absent in Gentzen's book. This is why I've introduced the plain
no_brackets print mode around 1998, which now happens to be the default in
Isabelle/jEdit after so many years.
There is also a broader perspective here: printing of rules can be done in
a high-level fashion via 'print_statement', but likewise printing of goal
states is still not available. The latter would also overcome
misunderstanding how to prove "!!x. A ==> B ==> C", i.e. by saying
"fix x assume A B show C", not show "!!x. A ==> B ==> C".
This archive was generated by a fusion of
Pipermail (Mailman edition) and