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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and