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.
- Projects
- None
- Subscribers
- None