Added abs_def attribute.
authorberghofe
Thu Jan 29 22:27:07 2009 +0100 (2009-01-29)
changeset 29690c81f8b2967e1
parent 29689 dd086f26ee4f
child 29691 9f03b5f847cd
Added abs_def attribute.
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Jan 29 15:29:41 2009 +0000
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jan 29 22:27:07 2009 +0100
     1.3 @@ -293,6 +293,8 @@
     1.4  val rotated = syntax
     1.5    (Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
     1.6  
     1.7 +val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def));
     1.8 +
     1.9  
    1.10  (* theory setup *)
    1.11  
    1.12 @@ -321,7 +323,8 @@
    1.13      ("rule_format", rule_format, "result put into standard rule format"),
    1.14      ("rotated", rotated, "rotated theorem premises"),
    1.15      ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
    1.16 -      "declaration of definitional transformations")]));
    1.17 +      "declaration of definitional transformations"),
    1.18 +    ("abs_def", abs_def, "abstract over free variables of a definition")]));
    1.19  
    1.20  
    1.21