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



2012-08-10 12:22 Brian Huffman:
Scanning the *ML* sources is probably not very useful.

Indeed – I realized my mistake (see my reply to Johannes where I explained why I ran into this wrong direction).

If you are looking for a specific lemma, you should definitely learn
the "find_theorems" command. See e.g. section 3.1.11 of the "Tutorial
on Isabelle/HOL".

Nice!

I should really be using ProofGeneral _and_ jEdit side-by-side. Shouldn't be a problem, as either editor notices when the other one has changed the file, and offers reloading.

Cheers,

Christoph

--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec, Skype duke4701

→ Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
  1 Feb 2013.  Deadline 2 Sep.  http://iaria.org/conferences2013/WEB13.html





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