Re: [isabelle] Length of Proofs
On Thu, 22 Nov 2012, Jeremy Dawson wrote:
Given that in HOL (as in Isabelle, both pre and post Isar) one can
always use proof procedures coded by someone else, this seems to sum up
to saying that Isabelle/Isar is like HOL, minus the capacity to code
one's own proof procedures, plus -- what ??
From where did you get the "minus"? Certainly not from this thread, where
I've pointed to the method_setup command of Isabelle/Isar already. It is
document in the "isar-ref" manual, as all other Isar commands. The
"implementation" manual has further documentation about what proof methods
are, compared to bare-bones tactics (which are also documented there).
The "plus" is much more than be discussed on such a mail thread. It also
depends on the imagination of users, what they make out of the vast formal
environment that Isabelle gives you today (as of current Isabelle2012).
This archive was generated by a fusion of
Pipermail (Mailman edition) and