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 happen?

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 good ones.


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


	Makarius





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