diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Recipes/ExternalSolver.thy
--- 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