# HG changeset patch
# User wenzelm
# Date 1011189877 -3600
# Node ID 1748c16c2df38df24427358a62c21d4df35ce319
# Parent  501da8288f05295e37698840d53096a776b7f565
norm_hhf;

diff -r 501da8288f05 -r 1748c16c2df3 src/Pure/Isar/attrib.ML
--- 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"),