Re: [isabelle] rule Unifies With Chained Facts?
On Mon, 4 Apr 2011, Brian Huffman wrote:
By anyone's standard, I would be considered an "expert" Isabelle user...
and in my years of experience with Isar I never knew this! How did that
There is no problem with that. In general there are many very delicate
points in Isar, but it is partly successful since it can be used without
going to the bottom of every detail. Instead, the usual way is to imitate
"best-style" proofs. Unfortunately, not all examples in the libraries are
How are average users expected to learn these things?
By being lucky in the selection of manuals or chosing the teacher. This
very issue of "initial method" vs. "terminal method" should also have been
mentioned quite often on the mailing list.
Since a couple of years, my tendency is to make the system guide users
more explicitly (e.g. in the Prover IDE), although I can also foresee lots
of complaints about such tutelage ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and