# 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
[A,B] [D]
C F G H I
------------------------
J
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 --> B
[A] [B]
A v B C C
---------------
C
which is not very different from Larry's bracket notation.
My 2 cents,
Christian

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*