Re: [isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features

On Wed, 30 May 2012, gottfried.barrow at wrote:

On 5/29/2012 2:29 AM, Lars Noschinski wrote:
On 26.05.2012 03:58, gottfried.barrow at wrote:
Being in the habit of using the Acrobat search is what messed me up. The
phrase "find_theorems" is listed in the index, but I had searched on
"find", and it didn't show up in the search, so I didn't even think
about the index.

Many PDF viewers choke on "fi", as generates an fi-ligature instead of two letters f and i.

I didn't know yet that Acrobat Reader could cause such extra problems. Which version is it?

The tiny Sumatra PDF browser that is now bundled with Isabelle2012 seems to be able to find and copy paste "find theorems" (without underscore) in isar-ref.pdf without problems. You get that by default when you invoke "isabelle doc isar-ref" in the Cygwin-Terminal. See also

Just on the day of the Isabelle2012 announcement Sumatra PDF was updated, which now causes some odd invitation to update when starting up the first time. The positive aspect is that this project seems to be quite active, so that the Windows platform now gets a PDF rendering engine of equal or better quality than Poppler on Linux.


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