--- a/src/Pure/Isar/attrib.ML Tue Jan 15 23:23:09 2002 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Jan 16 15:04:37 2002 +0100
@@ -288,6 +288,7 @@
(* misc rules *)
fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
+fun norm_hhf x = no_args (Drule.rule_attribute (K Tactic.norm_hhf)) x;
fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
@@ -308,6 +309,7 @@
("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
("folded", (folded_global, folded_local), "folded definitions"),
("standard", (standard, standard), "result put into standard form"),
+ ("norm_hhf", (norm_hhf, norm_hhf), "result put into HHF normal form"),
("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
("no_vars", (no_vars, no_vars), "frozen schematic vars"),
("consumes", (consumes, consumes), "number of consumed facts"),