author | wenzelm |
Mon, 16 Mar 2009 17:48:02 +0100 | |
changeset 30546 | b3b1f4184ae4 |
parent 30545 | 8209a7196389 |
child 30547 | 4c2514625873 |
--- a/doc-src/IsarRef/Thy/Spec.thy Mon Mar 16 17:47:26 2009 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Mon Mar 16 17:48:02 2009 +0100 @@ -878,7 +878,7 @@ let val th' = th OF ths in th' end)) *} "my rule" - attribute_setup my_declatation = {* + attribute_setup my_declaration = {* Attrib.thms >> (fn ths => Thm.declaration_attribute (fn th: thm => fn context: Context.generic => let val context' = context