Re: [isabelle] help



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.

By the way, if I use Isabelle/jEdit, do I need study Isar in chapter 4 of the doc?

Isar is one of the thing which make Isabelle so relevant. So yes, you really have to study Isar. Isar is for readable and expressive proof text (and what's more readable is more trustable), close enough to what you may see in some logic or maths books, although the concrete notation differs a lot, the structure is a lot similar. Learn Isar if you don't want to have proof looking like machine code.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





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