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



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.

Christoph: Searching for text in these pdf manual is not reliable; for example "fi" is turned into an fi-ligature (a single character), so it does not turn up when searching for fi (two characters), at least for some pdf readers.

It is far more reliable to look into the index at the end 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.






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