[isabelle] signature of ml_antiquotation.ML: inline, value, embedded, etc.



Dear list,

I fail to understand the signature provided by
`Pure/ML/ml_antiquotation.ML` (see below).
Can someone explain the meaning of `declaration`, `inline`, `value`, and
`special_form`? Moreover, what is the meaning of `embedded` (e.g.
`inline` vs `inline_embedded`)?

Best wishes,

Kevin

```
val value_decl: string -> string -> Proof.context ->
(Proof.context -> string * string) * Proof.context
val declaration: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string)
* Proof.context) ->
theory -> theory
val declaration_embedded: binding -> 'a context_parser ->
(Token.src -> 'a -> Proof.context -> (Proof.context -> string * string)
* Proof.context) ->
theory -> theory
val inline: binding -> string context_parser -> theory -> theory
val inline_embedded: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
val value_embedded: binding -> string context_parser -> theory -> theory
val special_form: binding -> string -> theory -> theory
```






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