src/Doc/Isar_Ref/Spec.thy
changeset 69913 ca515cf61651
parent 69597 ff784d5a5bfb
child 69962 82e945d472d5
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 16:35:58 2019 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Mar 14 16:55:06 2019 +0100
     1.3 @@ -93,8 +93,8 @@
     1.4    proof documents work properly. Command keywords need to be classified
     1.5    according to their structural role in the formal text. Examples may be seen
     1.6    in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close>
     1.7 -  \<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for
     1.8 -  theory-level declarations with and without proof, respectively. Additional
     1.9 +  \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for
    1.10 +  theory-level definitions with and without proof, respectively. Additional
    1.11    @{syntax tags} provide defaults for document preparation
    1.12    (\secref{sec:tags}).
    1.13