[isabelle-dev] NEWS: ML antiquotations for type constructors and term constants

[Florian Haftmann]

> * ML antiquotations for type constructors and term constants:
> 
>     \<^Type>‹c›
>     \<^Type>‹c T …›       ― ‹same with type arguments›
>     \<^Type>_fn‹c T …›    ― ‹fn abstraction, failure via exception TYPE›
>     \<^Const>‹c›
>     \<^Const>‹c T …›      ― ‹same with type arguments›
>     \<^Const>‹c for t …›  ― ‹same with term arguments›
>     \<^Const_>‹c …›       ― ‹same for patterns: case, let, fn›
>     \<^Const>_fn‹c T …›   ― ‹fn abstraction, failure via exception TERM›

Excellent!

The abstraction form syntax is not so trivial to grasp, maybe one
example coulde be added to the NEWS, e. g.

val dest_add_nat = \<^Const_fn>‹Groups.plus \<^Type>‹nat› for a b =>
‹(a, b)››

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20210929/dc18afbd/attachment.sig>