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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and