1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 06 19:13:48 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 06 22:02:34 2011 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  imports Base Main
     1.5  begin
     1.6  
     1.7 -chapter {* Theory specifications *}
     1.8 +chapter {* Specifications *}
     1.9  
    1.10  text {*
    1.11    The Isabelle/Isar theory format integrates specifications and
    1.12 @@ -922,14 +922,14 @@
    1.13        Thm.rule_attribute
    1.14          (fn context: Context.generic => fn th: thm =>
    1.15            let val th' = th OF ths
    1.16 -          in th' end)) *}  "my rule"
    1.17 +          in th' end)) *}
    1.18  
    1.19    attribute_setup my_declaration = {*
    1.20      Attrib.thms >> (fn ths =>
    1.21        Thm.declaration_attribute
    1.22          (fn th: thm => fn context: Context.generic =>
    1.23            let val context' = context
    1.24 -          in context' end)) *}  "my declaration"
    1.25 +          in context' end)) *}
    1.26  
    1.27  
    1.28  section {* Primitive specification elements *}