src/Doc/Isar_Ref/Spec.thy
changeset 66757 e32750d7acb4
parent 66248 df85956228c2
child 66916 aca50a1572c5
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 18:35:51 2017 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 02 19:28:18 2017 +0200
     1.3 @@ -1177,6 +1177,23 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 +section \<open>External file dependencies\<close>
     1.8 +
     1.9 +text \<open>
    1.10 +  \begin{matharray}{rcl}
    1.11 +    @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
    1.12 +  \end{matharray}
    1.13 +
    1.14 +  @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
    1.15 +
    1.16 +  \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
    1.17 +  name, such that the Isabelle build process knows about it (see also @{cite
    1.18 +  "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
    1.19 +  File.read}, without specific management by the Prover IDE.
    1.20 +\<close>
    1.21 +
    1.22 +
    1.23 +
    1.24  section \<open>Primitive specification elements\<close>
    1.25  
    1.26  subsection \<open>Sorts\<close>