Re: [isabelle] help
You will find documentation at
Start with the first one. For greater depth, or for reference, you could look at the second one. The remaining documents are specialised.
Isabelle/HOL refers to the higher-order logic instance of Isabelle, which practically everybody uses; Isar refers to the structured proof language in which proofs are written.
On 1 Mar 2013, at 11:27, liujing657949251 <liujing657949251 at 126.com> wrote:
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and