changeset 60317 | 9b7248379101 |
parent 60093 | c48d536231fe |
child 60371 | 8a5cfdda1b98 |
--- 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"