[isabelle] help

Dear all proof lovers:
I am really new to Isabelle. I hope to use Isabell/HOL for proving. Recently I am reading prog-prove in Isabelle.doc. Until now I have read half of it, but I am so puzzled that I really don't know how to combine the little examples in doc with the Isabelle/jEdit. 
They are just some fragments in one proof, I guess. So what should I do next? 
By the way, if I use Isabelle/jEdit, do I need study Isar in chapter 4 of the doc? 
My tutor told me to read some little examples, but I usually do not know why some lemmas should be proved first or some else. I do not know why I read the doc, but it doesn't help me to these question. 
So I really hope to know how to learn. 
Thank you very much!
Best wishes!
Liu Jing

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