equal
deleted
inserted
replaced
245 * Thm.instantiate, Thm.generalize and related operations require |
245 * Thm.instantiate, Thm.generalize and related operations require |
246 scalable datastructures from structure TVars, Vars, Names etc. |
246 scalable datastructures from structure TVars, Vars, Names etc. |
247 INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate |
247 INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate |
248 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable |
248 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable |
249 accumulation of items. |
249 accumulation of items. |
|
250 |
|
251 * ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline |
|
252 corresponding ML values, notably as arguments for Thm.instantiate etc. |
250 |
253 |
251 * The "build" combinators of various data structures help to build |
254 * The "build" combinators of various data structures help to build |
252 content from bottom-up, by applying an "add" function the "empty" value. |
255 content from bottom-up, by applying an "add" function the "empty" value. |
253 For example: |
256 For example: |
254 |
257 |