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



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.