equal
deleted
inserted
replaced
337 * Thm.instantiate, Thm.generalize and related operations require |
337 * Thm.instantiate, Thm.generalize and related operations require |
338 scalable datastructures from structure TVars, Vars, Names etc. |
338 scalable datastructures from structure TVars, Vars, Names etc. |
339 INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate |
339 INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate |
340 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable |
340 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable |
341 accumulation of items. |
341 accumulation of items. |
342 |
|
343 * ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline |
|
344 corresponding ML values, notably as arguments for Thm.instantiate etc. |
|
345 |
342 |
346 * ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to |
343 * ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to |
347 corresponding functions for the object-logic of the ML compilation |
344 corresponding functions for the object-logic of the ML compilation |
348 context. This supersedes older mk_Trueprop / dest_Trueprop operations. |
345 context. This supersedes older mk_Trueprop / dest_Trueprop operations. |
349 |
346 |