src/Doc/Isar_Ref/Spec.thy
changeset 66757 e32750d7acb4
parent 66248 df85956228c2
child 66916 aca50a1572c5
equal deleted inserted replaced
66756:a1b2ea991ad1 66757:e32750d7acb4
  1175   overhead. Relevant ML modules need to be compiled beforehand with debugging
  1175   overhead. Relevant ML modules need to be compiled beforehand with debugging
  1176   enabled, see @{attribute ML_debugger} above.
  1176   enabled, see @{attribute ML_debugger} above.
  1177 \<close>
  1177 \<close>
  1178 
  1178 
  1179 
  1179 
       
  1180 section \<open>External file dependencies\<close>
       
  1181 
       
  1182 text \<open>
       
  1183   \begin{matharray}{rcl}
       
  1184     @{command_def "external_file"} & : & \<open>any \<rightarrow> any\<close> \\
       
  1185   \end{matharray}
       
  1186 
       
  1187   @{rail \<open>@@{command external_file} @{syntax name} ';'?\<close>}
       
  1188 
       
  1189   \<^descr> \<^theory_text>\<open>external_file name\<close> declares the formal dependency on the given file
       
  1190   name, such that the Isabelle build process knows about it (see also @{cite
       
  1191   "isabelle-system"}). The file can be read e.g.\ in Isabelle/ML via @{ML
       
  1192   File.read}, without specific management by the Prover IDE.
       
  1193 \<close>
       
  1194 
       
  1195 
       
  1196 
  1180 section \<open>Primitive specification elements\<close>
  1197 section \<open>Primitive specification elements\<close>
  1181 
  1198 
  1182 subsection \<open>Sorts\<close>
  1199 subsection \<open>Sorts\<close>
  1183 
  1200 
  1184 text \<open>
  1201 text \<open>