[isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

Makarius makarius at sketis.net
Wed Oct 8 20:46:52 CEST 2014

*** ML ***

* Basic combinators map, fold, fold_map, split_list are available as
parameterized antiquotations, e.g. @{map 4} for lists of quadruples.

This refers to Isabelle/9f10d82e8188.

After seeing another split_list42 combinator, I could not resist to make a 
fully general solution once and for all.  The changset also eliminates 
some clones that have accumulated over the years.

Isabelle/ML has antiquotations as some kind of macro language.  It can do 
certain things better than the C preprocessor, although one always needs 
to be careful to stay within reason.



More information about the isabelle-dev mailing list