Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: ML antiquotations for object-logic j...

Email Gateway (Sep 22 2021 at 10:55):

From: Makarius <makarius@sketis.net>
* 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
https://isabelle-dev.sketis.net/rISABELLE5d411d85da8c

Makarius

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Last updated: Feb 01 2025 at 20:19 UTC