unused;
authorwenzelm
Sat, 30 May 2015 22:18:12 +0200
changeset 60317 9b7248379101
parent 60316 e487b83a9885
child 60318 ab785001b51d
unused;
src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat May 30 22:04:15 2015 +0200
+++ b/src/Pure/Pure.thy	Sat May 30 22:18:12 2015 +0200
@@ -186,10 +186,6 @@
     in th' end))\<close>
   "imported schematic variables"
 
-attribute_setup eta_long =
-  \<open>Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))\<close>
-  "put theorem into eta long beta normal form"
-
 attribute_setup atomize =
   \<open>Scan.succeed Object_Logic.declare_atomize\<close>
   "declaration of atomize rule"