[isabelle] Fw : Re: Question on hypothesis



how to do when I have a conjunction of hypothesis to simplify 
I have tried :
theory Scratch
  imports Main
  begin
example_proof
have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)"  apply simp
 
but it doesn't work.
 
Best Regards.








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