[isabelle] help

Dear all proof lovers:
I am really new to Isabelle. Recently I hope to learn HOL and try to use automatic therom prover. So I download the Isabelle2013. Now I hope to use Isabelle/jEdit in Windows OS for therom proving. However, what make me confused is, what is the difference between Isabelle/HOL and Isabelle/Isar? And what syntax should I learn, Isabelle/Isar syntax or Isabelle/HOL syntax? Please tell me the specific tutorial I should learn. 
Here, I am learning the simple example, which is in appendix. Am I right?
Thanks very much.

Liu Jing

Attachment: Seq.thy
Description: Binary data

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