[isabelle-dev] record pretty printing

Gerwin Klein gerwin.klein at nicta.com.au
Wed Feb 13 10:18:40 CET 2008

Florian Haftmann wrote:
> Since this is part of the syntax layer,
> 	val unit = (fn Const (@{const_syntax Product_Type.Unity},__) => true |
> _ => false);
> is the appropriate antiquotation.


It's not entirely satisfying (I was hoping I could get away with not 
mentioning Product_Type), but better than what I had before. I'll commit 
this then.

> \<^const> indicates authentic constant syntax.

Ok. Now (I think) I understand the NEWS entry about authentic mode ;-)
NEWS on its own really is sometimes too cryptic.


More information about the isabelle-dev mailing list