*** 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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
