Re: [isabelle] PIDE Display of Assumptions
On Fri, 29 Jun 2012, Patrick Michel wrote:
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.
See the isar-ref manual for all commands. The 'help' command also gives
you a complete list. These things were well-known before Proof General
introduced some menus for some commands > 10 years ago.
What you want here is 'find_theorems'. Apart from the full syntax the
manual also gives you 'find_consts', which Proof General does not know
because that command is younger than 5 years.
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.
Historically, Larry Paulson introduced the brackets notation both for ==>
and => and used it mainly in Isabelle/ZF. Later Isabelle/HOL became more
popular, and the custom to use brackets for ==> but not for =>.
When I was exposed to this for the first time in 1993, I made sure that
brackets do work uniformly as expected, because the pretty printer was not
working in all situations at that time. Around 1998 I then learned how to
make Isabelle/Pure rules nest properly (which was not possible before),
and found the brackets very difficult to read. E.g. in your example
above, the first two goal premises are nested ==> which you see
immediately from the parentheses in the first output, but not in the
Anyway, print modes like "brackets", "no_brackets", "type_brackets",
"no_type_brackets" are there to make output more interesting by
individualizing it. There is also a mode "iff" for boolean equality as
double arrow, which is off by default.
This archive was generated by a fusion of
Pipermail (Mailman edition) and