[isabelle] PIDE Display of Assumptions


While updating my theories to Isabelle/HOL 2012 (worked like a charm) I was also trying out PIDE.
I am quite happy with the IDE so far, once I figured 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?


Patrick Michel
Software Technology Group
University of Kaiserslautern

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