Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?



2012-08-10 14:01 Lars Noschinski:
Christoph: Searching for text in these pdf manual is not reliable; for
example "fi" is turned into an fi-ligature (a single character), so it
does not turn up when searching for fi (two characters), at least for
some pdf readers.

Good point – I didn't realize, as I mainly use PDF viewers that support them. But indeed I see that Adobe Reader doesn't.

This post might be helpful: http://www.acsu.buffalo.edu/~jfernand/archives/2011/01/allow-adobe-reader-to-find-words-containing-ligatures.html (note the link to glyphtounicode.tex is broken, but Google will find it, and many TeX installations have it)

I'm not sure whether this solution is generally applicable, but maybe the LaTeX-to-PDF creation workflow of Isabelle could be adapted to take this fix into account. (This won't fix the unterscore problem yet.)


It is far more reliable to look into the index at the end of the
reference manual.

Uh – I hope I won't eventually have to _print_ the manual ;-)

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
  1 Feb 2013.  Deadline 2 Sep.  http://iaria.org/conferences2013/WEB13.html





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