Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed attribute "norm_hhf";
authorwenzelm
Wed, 24 Jul 2002 00:11:56 +0200
changeset 13414 15597d502035
parent 13413 0b60b9e18a26
child 13415 63462ccc6fac
removed attribute "norm_hhf";
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Wed Jul 24 00:11:24 2002 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Jul 24 00:11:56 2002 +0200
@@ -288,7 +288,6 @@
 (* 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_rule)) 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;
 
@@ -342,7 +341,6 @@
   ("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"),
isabelle