--- a/ProgTutorial/Recipes/ExternalSolver.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy Tue May 14 11:10:53 2019 +0200
@@ -28,8 +28,8 @@
one second:
@{ML_response_fake [display,gray]
- "TimeLimit.timeLimit (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
- handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+ "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
+ handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
applications, e.g. coupling external solvers with Isabelle. In that case,