diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Fri May 17 10:38:01 2019 +0200
@@ -33,7 +33,7 @@
 text \<open>
   then the resulting propositional formula @{ML pform} is 
   
-  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} 
+  @{ML [display] \<open>Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)\<close> in Prop_Logic} 
   
 
   where indices are assigned for the variables 
@@ -43,8 +43,8 @@
   input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
 
   @{ML_matchresult_fake [display,gray]
-  "Termtab.dest table"
-  "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
+  \<open>Termtab.dest table\<close>
+  \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>}
 
   An index is also produced whenever the translation
   function cannot find an appropriate propositional formula for a term. 
@@ -55,22 +55,22 @@
        Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty\<close>
 
 text \<open>
-  returns @{ML "BoolVar 1" in Prop_Logic} for  @{ML pform'} and the table 
+  returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
   @{ML_matchresult_fake [display,gray]
-  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
-  "(\<forall>x. P x, 1)"}
+  \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+  \<open>(\<forall>x. P x, 1)\<close>}
   
   In the print out of the tabel, we used some pretty printing scaffolding 
   to see better which assignment the table contains.
  
   Having produced a propositional formula, you can now call the SAT solvers 
-  with the function @{ML "SAT_Solver.invoke_solver"}. For example
+  with the function @{ML \<open>SAT_Solver.invoke_solver\<close>}. For example
 
   @{ML_matchresult_fake [display,gray]
-  "SAT_Solver.invoke_solver \"minisat\" pform"
-  "SAT_Solver.SATISFIABLE assg"}
+  \<open>SAT_Solver.invoke_solver "minisat" pform\<close>
+  \<open>SAT_Solver.SATISFIABLE assg\<close>}
 \<close>
 
 text \<open>
@@ -78,12 +78,12 @@
   the returned function \<open>assg\<close>
 
   @{ML_matchresult [display,gray]
-"let
-  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
+\<open>let
+  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver "auto" pform
 in 
   (assg 1, assg 2, assg 3)
-end"
-  "(NONE, SOME true, NONE)"}
+end\<close>
+  \<open>(NONE, SOME true, NONE)\<close>}
 
   we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close>
   that makes the formula satisfiable. 
@@ -102,7 +102,7 @@
 done
 
 text \<open>
-  However, for proving anything more exciting using @{ML "sat_tac" in SAT} you 
+  However, for proving anything more exciting using @{ML \<open>sat_tac\<close> in SAT} you 
   have to use a SAT solver that can produce a proof. The internal 
   one is not usuable for this.