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 second.

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.


	Makarius


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