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



On Fri, 10 Aug 2012, Christoph LANGE wrote:

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.

See also this thread: https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-May/msg00251.html


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

You can post whatever you want on this list, as long as it refers to the
official Isabelle release -- normally the latest one, or one or two versions behind.

It also helps to search the mailing list archives. See the links on the Isabelle website front page.


BTW, after more than 25 years certain things in Isabelle are just as they are to the good or to the confusion of new users. "Bugs" are very rare -- often it is just a misunderstanding what to expect.

Of course it always helps if you report your observations and share the experience to get things the way you need them.


	Makarius


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