*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Makarius <makarius at sketis.net>*Date*: Fri, 10 Aug 2012 16:52:56 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5024F90E.2030505@cs.bham.ac.uk>*References*: <5024ABB2.8010900@cs.bham.ac.uk> <CAAMXsiayP7z=SKiXA3bhQ0iav_AMqdJDEU+itHRTKTgOMGZs-w@mail.gmail.com> <5024DD89.3010508@cs.bham.ac.uk> <1344594145.1841.79.camel@macbroy12.informatik.tu-muenchen.de> <5024EF67.9040308@cs.bham.ac.uk> <5024F165.8030401@in.tum.de> <5024F3B3.7070109@in.tum.de> <5024F90E.2030505@cs.bham.ac.uk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 cantry it by searching the PDF for "find_theorems".doc-src/IsarRef/Thy/Misc.thy doesn't contain anything suspicious, so Isuspect a bug in the document preparation implementation.

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

Makarius

**References**:**[isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Christoph LANGE

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

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

**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Johannes Hölzl

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

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

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

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

- Previous by Date: Re: [isabelle] type_synonym
- Next by Date: Re: [isabelle] type_synonym
- Previous by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list