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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and