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

[Makarius]

On 29/09/2021 11:43, Florian Haftmann wrote:
>> * 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)››

In Isabelle/b9331caf92c3, I have updated the above examples using
Type_fn/Const_fn (they were from an earlier stage, before these extra
antiquotations).

Also note that in Isabelle/e585e5a906ba, I have tune the syntax to allow the
\<^Type>‹nat› in your example stand on its own, without an extra cartouche
around it.


	Makarius