Re: [isabelle] help



You will find documentation at

http://isabelle.in.tum.de/documentation.html

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.

Larry Paulson


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
> 
> 
> 
> 
> 
> <Seq.thy>






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