[isabelle] Question on hypothesis










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.








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