--- a/ProgTutorial/Recipes/ExternalSolver.thy Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy Tue May 14 17:10:47 2019 +0200
@@ -3,9 +3,9 @@
begin
-section {* Executing an External Application (TBD) \label{rec:external}*}
+section \<open>Executing an External Application (TBD) \label{rec:external}\<close>
-text {*
+text \<open>
{\bf Problem:}
You want to use an external application.
\smallskip
@@ -36,18 +36,18 @@
one has to make sure that Isabelle can find the particular executable.
One way to ensure this is by adding a Bash-like variable binding into
one of Isabelle's settings file (prefer the user settings file usually to
- be found at @{text "$HOME/.isabelle/etc/settings"}).
+ be found at \<open>$HOME/.isabelle/etc/settings\<close>).
- For example, assume you want to use the application @{text foo} which
- is here supposed to be located at @{text "/usr/local/bin/"}.
+ For example, assume you want to use the application \<open>foo\<close> which
+ is here supposed to be located at \<open>/usr/local/bin/\<close>.
The following line has to be added to one of Isabelle's settings file:
- @{text "FOO=/usr/local/bin/foo"}
+ \<open>FOO=/usr/local/bin/foo\<close>
In Isabelle, this application may now be executed by
@{ML_response_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
-*}
+\<close>
end