equal
deleted
inserted
replaced
333 text \<open> |
333 text \<open> |
334 In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close> |
334 In order to demonstrate batch execution of Isabelle, we retrieve the \<^verbatim>\<open>Main\<close> |
335 theory value from the theory loader within ML (observe the delicate quoting |
335 theory value from the theory loader within ML (observe the delicate quoting |
336 rules for the Bash shell vs.\ ML): |
336 rules for the Bash shell vs.\ ML): |
337 @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>} |
337 @{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main"' HOL\<close>} |
338 |
|
339 Note that the output text will be interspersed with additional junk messages |
|
340 by the ML runtime environment. |
|
341 \<close> |
338 \<close> |
342 |
339 |
343 |
340 |
344 section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
341 section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close> |
345 |
342 |