author | wenzelm |
Sat, 30 May 2015 22:18:12 +0200 | |
changeset 60317 | 9b7248379101 |
parent 60316 | e487b83a9885 |
child 60318 | ab785001b51d |
src/Pure/Pure.thy | file | annotate | diff | comparison | revisions |
--- 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"