*To*: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso at ens-lyon.fr>*Subject*: Re: [isabelle] unknow theorem*From*: Amine Chaieb <chaieb at informatik.tu-muenchen.de>*Date*: Tue, 18 Jul 2006 14:36:05 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20060717150416.64mgwa2jwd8g0k40@mouette.ens-lyon.fr>*References*: <20060717150416.64mgwa2jwd8g0k40@mouette.ens-lyon.fr>

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.

**Follow-Ups**:**Re: [isabelle] unknow theorem***From:*Francisco Jose Chaves Alonso

**[isabelle] locale default structure***From:*Peter Lammich

**References**:**[isabelle] unknow theorem***From:*Francisco Jose Chaves Alonso

- Previous by Date: Re: [isabelle] Isabelle + Alice
- Next by Date: Re: [isabelle] unknow theorem
- Previous by Thread: [isabelle] unknow theorem
- Next by Thread: Re: [isabelle] unknow theorem
- Cl-isabelle-users July 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list