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



On 8/1/2012 9:18 PM, Christian Sternagel wrote:
- HOL syntax is defined via commands (not sure whether those are really part of Isar or rather independent; my guess would be that they are just convenience tools built on top of the Isabelle/ML layer... but then, what is not?)

This calls for a "dude expression" using "dude syntax" interpreted with standard "dude semantics", as in, "Man, dude, if you (meaning me) would only open the source files and do some brainless scrolling around, you wouldn't clutter up the list with as many emails for a single subject."

At the bottom of ~/src/HOL/Tools/Datatype/datatype.ML, we get this:

val _ =
Outer_Syntax.command @{command_spec "datatype"} "define inductive datatypes"
    (Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));

So some HOL syntax is defined with Isar commands, and some HOL syntax is defined with ML, where some HOL syntax is added as outer syntax.

Regards,
GB








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