306 ("where", (where_global, where_local), "named instantiation of theorem"), |
307 ("where", (where_global, where_local), "named instantiation of theorem"), |
307 ("of", (of_global, of_local), "rule applied to terms"), |
308 ("of", (of_global, of_local), "rule applied to terms"), |
308 ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"), |
309 ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"), |
309 ("folded", (folded_global, folded_local), "folded definitions"), |
310 ("folded", (folded_global, folded_local), "folded definitions"), |
310 ("standard", (standard, standard), "result put into standard form"), |
311 ("standard", (standard, standard), "result put into standard form"), |
|
312 ("norm_hhf", (norm_hhf, norm_hhf), "result put into HHF normal form"), |
311 ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"), |
313 ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"), |
312 ("no_vars", (no_vars, no_vars), "frozen schematic vars"), |
314 ("no_vars", (no_vars, no_vars), "frozen schematic vars"), |
313 ("consumes", (consumes, consumes), "number of consumed facts"), |
315 ("consumes", (consumes, consumes), "number of consumed facts"), |
314 ("case_names", (case_names, case_names), "named rule cases"), |
316 ("case_names", (case_names, case_names), "named rule cases"), |
315 ("params", (params, params), "named rule parameters"), |
317 ("params", (params, params), "named rule parameters"), |