*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?*From*: Makarius <makarius at sketis.net>*Date*: Mon, 21 May 2012 11:24:33 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk, Oleksandr Gavenko <gavenkoa at gmail.com>*In-reply-to*: <4FB99589.7090809@rsise.anu.edu.au>*References*: <87havcyn5p.fsf@desktop.home.int> <CANofLe+qNjhzCpQP41OE+dLh8LLPAZpXRN8YezngkygnoOWL+Q@mail.gmail.com> <87bolia9gu.fsf@desktop.home.int> <4FB99589.7090809@rsise.anu.edu.au>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 21 May 2012, Jeremy Dawson wrote:

Fortunately the extra effort is just repetitive grunt work for whichIsabelle's SML user interface is ideally suited. Unfortunately you willno doubt have been led to believe that the SML user interface is not theway to go in using Isabelle.

Makarius

**References**:**[isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

**Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Randy Pollack

**Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

**Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] isabelle2012-rc3\isabelle.exe removed by Norton when executed
- Next by Date: Re: [isabelle] $HOME, $USER_HOME, and how I call "bin/isabelle" commands with batch/bash files
- Previous by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Next by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list