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



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.