Re: [isabelle] Length of Proofs
I don't suppose the legacy code simply can't be ported, any more than it
can't be translated into HOL. But when I started to port it from
Isabelle2005 to Isabelle2007 (still using ML tactics) I quickly gave
up. I expect it would be much worse now.
And although it seems as though the documentation is more extensive now
than it was then, to learn Isar I would anticipate having some
questions. And the sort of answers I've had in the past to questions
("look at Makarius's thesis") aren't encouraging. The point is that to
contemplate converting everything to Isar I need to _know_ that help
will be available.
And anyway, what is the point of a system where you write tactics and
then wrap them up as required to give them the type required by
method_setup, rather than just write tactics? (This is of course a
question to which the answer might be apparent if there was a more
accessible description of the structure of an Isar proof than Makarius's
thesis). Or learning something as totally weird as the grammar of the
Lawrence Paulson wrote:
I think it's a great pity that you are using such an elderly version of Isabelle.
If you have a lot of legacy code that simply can't be ported, or an application where it works really well, okay. But for general proofs, there is simply no comparison between the Isabelle of today and one that is seven years old. Sledgehammer, counterexample finding, a very powerful function definition package, lots and lots of AFP theories… You shouldn't forego all of those.
This archive was generated by a fusion of
Pipermail (Mailman edition) and