author | webertj |
Mon, 11 Feb 2013 11:38:16 +0100 | |
changeset 52217 | 36aee533d7a7 |
parent 52216 | 0ee6039d2c8e |
child 52218 | e7b54119c436 |
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