> * 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
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
