HomeIsabelle/Phabricator
ML antiquotations for object-logic judgement

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.

Written by makarius on Sep 22 2021, 12:52 PM.
User
Projects
None
Subscribers
None

Event Timeline