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 126.com> 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