260 val pure_attributes = |
260 val pure_attributes = |
261 [("tag", (gen_tag, gen_tag), "tag theorem"), |
261 [("tag", (gen_tag, gen_tag), "tag theorem"), |
262 ("untag", (gen_untag, gen_untag), "untag theorem"), |
262 ("untag", (gen_untag, gen_untag), "untag theorem"), |
263 ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"), |
263 ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"), |
264 ("RS", (global_RS, local_RS), "resolve with rule"), |
264 ("RS", (global_RS, local_RS), "resolve with rule"), |
265 ("APP", (global_APP, local_APP), "resolve rule with"), |
265 ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"), |
266 ("where", (global_where, local_where), "named instantiation of theorem"), |
266 ("where", (global_where, local_where), "named instantiation of theorem"), |
267 ("with", (global_with, local_with), "positional instantiation of theorem"), |
267 ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"), |
268 ("standard", (standard, standard), "put theorem into standard form"), |
268 ("standard", (standard, standard), "put theorem into standard form"), |
269 ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"), |
269 ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"), |
270 ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")]; |
270 ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")]; |
271 |
271 |
272 |
272 |