Re: [isabelle] help

On Sun, 17 Mar 2013, Yannick Duchêne (Hibou57) wrote:

Le Sat, 16 Mar 2013 10:34:00 +0100, liujing657949251 <liujing657949251 at> a écrit:

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.

When you read the PDF doc, see an interesting sample and then want to give it a try in Isabelle/jEdit, be aware the text you may copy/past from the PDF to jEdit, may often be incorrect. Better learn Isar, to be able to input the samples directly in Isabelle/jEdit.

My example for first exposure is Isabelle2013/src/HOL/ex/Seq.thy -- you can open that file directly in Isabelle/jEdit. That is just a totally arbitrary entry point to a huge amount of Isabelle material.

Copy-paste from latex-generated PDF is indeed a black art. To avoid it, you can look through Isabelle2013/src/Doc/ although that material might occasionally look a bit odd in source form.


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