# HG changeset patch
# User berghofe
# Date 1233264427 -3600
# Node ID c81f8b2967e1097c63937b9d11d8760791ed4ebe
# Parent  dd086f26ee4f13696718b779fd8eab0405754a19
Added abs_def attribute.

diff -r dd086f26ee4f -r c81f8b2967e1 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jan 29 15:29:41 2009 +0000
+++ b/src/Pure/Isar/attrib.ML	Thu Jan 29 22:27:07 2009 +0100
@@ -293,6 +293,8 @@
 val rotated = syntax
   (Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
 
+val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def));
+
 
 (* theory setup *)
 
@@ -321,7 +323,8 @@
     ("rule_format", rule_format, "result put into standard rule format"),
     ("rotated", rotated, "rotated theorem premises"),
     ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
-      "declaration of definitional transformations")]));
+      "declaration of definitional transformations"),
+    ("abs_def", abs_def, "abstract over free variables of a definition")]));