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

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