[isabelle-dev] NEWS: ML antiquotations for object-logic judgement

Makarius makarius at sketis.net
Wed Sep 22 12:55:21 CEST 2021

*** ML ***

* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
corresponding functions for the object-logic of the ML compilation
context. This supersedes older mk_Trueprop / dest_Trueprop operations.

This refers to Isabelle/4974c3697fee.

It is just a fine point in recent "clarification of antiquotations", e.g. see
the impact on FOL and fologic.ML


More information about the isabelle-dev mailing list