*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 10 Aug 2012 14:01:00 +0200*In-reply-to*: <5024F165.8030401@in.tum.de>*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.5) Gecko/20120624 Icedove/10.0.5

On 10.08.2012 13:32, Tobias Nipkow wrote:

My mistake, will fix that, thanks!

find_theorems is explained on page 163 of the reference manual.

-- Lars

Am 10/08/2012 13:24, schrieb Christoph LANGE:BTW in the documentation find_theorems is only mentioned in prog-prove.pdf (just searched all files with pdfgrep), and there it says: --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- Command find_theorems searches for specific theorems in the current theory. Search criteria include pattern matching on terms and on names. For details see the Isabelle/Isar Reference Manual [4]. --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- … but the reference manual does't mention it.

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

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

- Previous by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- 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