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.


	Makarius





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