doc-src/IsarRef/Thy/Spec.thy
changeset 36178 0e5c133b48b6
parent 36177 8e0770d2e499
child 36454 f2b5bcc61a8c
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:15:09 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Apr 16 22:18:59 2010 +0200
     1.3 @@ -953,7 +953,7 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcll}
     1.7 -    @{command_def "types"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8 +    @{command_def "types"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    1.10      @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    1.11    \end{matharray}