[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?
Software Technology Group
University of Kaiserslautern
This archive was generated by a fusion of
Pipermail (Mailman edition) and