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

2012-08-10 13:42 Dmitriy Traytel:
I don't see the mistake. The Isabelle/Isar Reference Manual describes
find theorems on pages 163-165.

Indeed – but strangely this text is not searchable. The underscore of, e.g., find_theorems, is not represented as a usual underscore. You can try it by searching the PDF for "find_theorems". doc-src/IsarRef/Thy/Misc.thy doesn't contain anything suspicious, so I suspect a bug in the document preparation implementation.

Is this list the right way to report bugs, or is there any better way?

Cheers, and thanks,


Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
  1 Feb 2013.  Deadline 2 Sep.

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