Re: [isabelle] unknow theorem



Hi,

Strange. When i write 
 thm mult_mono

I get the theorem (So Isabelle finds it in the Database)
and

apply (rule mult_mono)
returns

goal (lemma, 4 subgoals):
 1. 0  Lb X; 0  Lb Y; Lb X  x; x  Ub X; Lb Y  y; y  Ub Y d Lb X  x
 2. 0  Lb X; 0  Lb Y; Lb X  x; x  Ub X; Lb Y  y; y  Ub Y d Lb Y  y
 3. 0  Lb X; 0  Lb Y; Lb X  x; x  Ub X; Lb Y  y; y  Ub Y d 0  x
 4. 0  Lb X; 0  Lb Y; Lb X  x; x  Ub X; Lb Y  y; y  Ub Y d 0  Lb Y

NB: I don't have the defs of Lb and Ub...

Which Version are you using?

> Where can I find the theorems for prove
> inequalities of reals?

Generally Ring_and_Fields.thy is the right place to look in. What i often 
Do is also to use the theorem search facility, see Section 5.14 of the 
Tutorial (http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf).

Hope it helps.
Amine.





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