Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
On Mon, 21 May 2012, Jeremy Dawson wrote:
Fortunately the extra effort is just repetitive grunt work for which
Isabelle's SML user interface is ideally suited. Unfortunately you will
no doubt have been led to believe that the SML user interface is not the
way to go in using Isabelle.
Why? Isabelle/ML and Isabelle/Isar are both the main Isabelle "user
interface", independently of the number of users who have ever writting
their own proof tools in ML. See also the command 'method_setup' in the
isar-ref manual to get started, and maybe search for some of its uses in
the Isabelle library.
Also note that in Isabelle/jEdit you get IDE functionality for both ML and
Isar source language, but of course you have to put your ML into the
proper formal context within a theory.
This archive was generated by a fusion of
Pipermail (Mailman edition) and