Re: [isabelle] Syntax issue: lost between HOL and Isar



ML is a programming language. You write programs in ML.

Pure is not a programming language. It is a logical formalism, specifically, the logical framework that is the basis of Isabelle.

HOL is also a programming language, namely higher-order logic.

Isar is a formal language for proof developments. These are not programs and it is not a programming language.

Larry Paulson


On 2 Aug 2012, at 16:46, Gottfried Barrow wrote:

> One last comment, hopefully.
> 
> Outer_syntax is defined in src/Pure/Isar/outer_syntax.ML:
> 
>    (*  Title:      Pure/Isar/outer_syntax.ML
>        Author:     Markus Wenzel, TU Muenchen
> 
>    The global Isabelle/Isar outer syntax.
> 
> I was wanting to start using the phrase "the Pure programming language", but "Outer_syntax.command" is an Isar command, so the HOL outer syntax "datatype" is defined as HOL syntax using an Isar command.
> 
> My use of "the Pure programming language" will have to wait until I understand whether there's any HOL syntax which can be defined using ML, but which cannot be defined using Isar.
> 
> I like to have the vocabulary locked down. I go with these ideas until someone tells me different.
> 
> Regards,
> GB
> 
> 
> 






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