Re: [isabelle] unknow theorem
Strange. When i write
I get the theorem (So Isabelle finds it in the Database)
apply (rule mult_mono)
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
Hope it helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and