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



I don't see the mistake. The Isabelle/Isar Reference Manual describes find theorems on pages 163-165.

Dmitriy

On 10.08.2012 13:32, Tobias Nipkow wrote:
My mistake, will fix that, thanks!

Tobias

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.






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