Typo in description of abs_def.
authorwebertj
Mon, 11 Feb 2013 11:38:16 +0100
changeset 5221736aee533d7a7
parent 52216 0ee6039d2c8e
child 52218 e7b54119c436
Typo in description of abs_def.
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Feb 08 16:41:04 2013 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Feb 11 11:38:16 2013 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4    setup (Binding.name "abs_def")
     1.5      (Scan.succeed (Thm.rule_attribute (fn context =>
     1.6        Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
     1.7 -    "abstract over free variables of definitionial theorem"));
     1.8 +    "abstract over free variables of definitional theorem"));
     1.9  
    1.10  
    1.11