diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Recipes/ExternalSolver.thy
--- a/CookBook/Recipes/ExternalSolver.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-theory ExternalSolver
-imports "../Base"
-begin
-
-
-section {* Executing an External Application \label{rec:external}*}
-
-text {*
-  {\bf Problem:}
-  You want to use an external application.
-  \smallskip
-
-  {\bf Solution:} The function @{ML system_out} might be the right thing for
-  you.
-  \smallskip
-
-  This function executes an external command as if printed in a shell. It
-  returns the output of the program and its return value.
-
-  For example, consider running an ordinary shell commands:
-
-  @{ML_response [display,gray] 
-    "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
-
-  Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
-  on Page~\pageref{rec:timeout}), i.e. external applications are killed
-  properly. For example, the following expression takes only approximately
-  one second:
-
-  @{ML_response [display,gray] 
-    "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
-     handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
-*}
-
-text {*
-  The function @{ML system_out} can also be used for more reasonable
-  applications, e.g. coupling external solvers with Isabelle. In that case,
-  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"}).
-  
-  For example, assume you want to use the application @{text foo} which
-  is here supposed to be located at @{text "/usr/local/bin/"}.
-  The following line has to be added to one of Isabelle's settings file:
-
-  @{text "FOO=/usr/local/bin/foo"}
-
-  In Isabelle, this application may now be executed by
-
-  @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
-*}
-
-
-end
\ No newline at end of file