*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Question on hypothesis*From*: olfa mraihi <olfa.mraihi at yahoo.fr>*Date*: Fri, 3 Dec 2010 01:04:54 +0000 (GMT)

Hi Isabelle community, I' m newbie on using Isabelle and I need you help by answering if possible these 2 questions: 1)how to represent hypothesis in isabelle? is it with the keyword "assume"? 2)how to tell isabelle to simplify a set of hypothesis under the use of the adequate theory? (remark:there is no goal to prove,only hypothesis to simplify),is it like that?: use_thy "theoryname.thy"; assume a & b & c; by auto; Thank you very much.

**Follow-Ups**:**Re: [isabelle] Question on hypothesis***From:*Makarius

- Previous by Date: [isabelle] Question on Goal and on Use_thy. Thank you.
- Next by Date: [isabelle] Cygwin/jEdit works
- Previous by Thread: Re: [isabelle] Question on Goal and on Use_thy. Thank you.
- Next by Thread: Re: [isabelle] Question on hypothesis
- Cl-isabelle-users December 2010 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