# HG changeset patch
# User berghofe
# Date 1115225439 -7200
# Node ID 09fad9a8bc47fe5e8a5652f30218ad4f1e2635b5
# Parent  f13f4694c36dda094f29c888a74089641081f81c
Added eta_long attribute.

diff -r f13f4694c36d -r 09fad9a8bc47 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed May 04 18:50:21 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed May 04 18:50:39 2005 +0200
@@ -444,6 +444,7 @@
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) 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;
+fun eta_long x = no_args (Drule.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;
 
 
 (* rule declarations *)
@@ -506,6 +507,7 @@
   ("standard", (standard, standard), "result put into standard form"),
   ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
+  ("eta_long", (eta_long, eta_long), "put theorem into eta long beta normal form"),
   ("consumes", (consumes, consumes), "number of consumed facts"),
   ("case_names", (case_names, case_names), "named rule cases"),
   ("params", (params, params), "named rule parameters"),