*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Patrick Michel <uni at pbmichel.de>*Subject*: Re: [isabelle] PIDE Display of Assumptions*From*: Makarius <makarius at sketis.net>*Date*: Fri, 29 Jun 2012 17:27:56 +0200 (CEST)*In-reply-to*: <21D0C044-1E6F-4EA7-8572-A97BE523796C@pbmichel.de>*References*: <21D0C044-1E6F-4EA7-8572-A97BE523796C@pbmichel.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 29 Jun 2012, Patrick Michel wrote:

While updating my theories to Isabelle/HOL 2012 (worked like a charm) Iwas also trying out PIDE. I am quite happy with the IDE so far, once Ifigured out how to search for theorems, etc.

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.

Makarius

**Follow-Ups**:**Re: [isabelle] PIDE Display of Assumptions***From:*Tobias Nipkow

**Re: [isabelle] PIDE Display of Assumptions***From:*Christian Urban

**Re: [isabelle] PIDE Display of Assumptions***From:*Makarius

**References**:**[isabelle] PIDE Display of Assumptions***From:*Patrick Michel

- Previous by Date: Re: [isabelle] making use of star
- Next by Date: Re: [isabelle] PIDE Display of Assumptions
- Previous by Thread: [isabelle] PIDE Display of Assumptions
- Next by Thread: Re: [isabelle] PIDE Display of Assumptions
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list