Re: [isabelle] PIDE Display of Assumptions
On Friday, June 29, 2012 at 16:27:56 (+0100), Makarius wrote:
> > At the moment, however, the curried notation of the meta implication drives me crazy :-)
> > My current subgoal structurally looks like this:
> > (A ⟹ B ⟹ C) ⟹ (D ⟹ F) ⟹ G ⟹ H ⟹ I ⟹ J
> > and I'd rather have it like this again:
> > [[A; B] ⟹ C; D ⟹ F; G; H; I] ⟹ J
> > Is there a display option for this?
> This is called "print mode" in Isabelle terminology. E.g.
> isabelle jedit -m brackets
> will recover the above special Isabelle syntax for nested implications.
Is there a way to make that printmode the default
in ones etc/settings, for example? 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.
My 2 cents,
This archive was generated by a fusion of
Pipermail (Mailman edition) and