--- a/ProgTutorial/Recipes/Sat.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Tue May 14 17:10:47 2019 +0200
@@ -3,9 +3,9 @@
 imports "../Appendix" "../First_Steps" 
 begin
 
-section {* SAT Solvers\label{rec:sat} *}
+section \<open>SAT Solvers\label{rec:sat}\<close>
 
-text {*
+text \<open>
   {\bf Problem:}
   You like to use a SAT solver to find out whether
   an Isabelle formula is satisfiable or not.\smallskip
@@ -25,19 +25,19 @@
   term into a propositional formula. Let
   us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. 
   The function will return a propositional formula and a table. Suppose 
-*}
+\<close>
 
-ML %grayML{*val (pform, table) = 
-       Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
+ML %grayML\<open>val (pform, table) = 
+       Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty\<close>
 
-text {*
+text \<open>
   then the resulting propositional formula @{ML pform} is 
   
   @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} 
   
 
   where indices are assigned for the variables 
-  @{text "A"} and @{text "B"}, respectively. This assignment is recorded 
+  \<open>A\<close> and \<open>B\<close>, respectively. This assignment is recorded 
   in the table that is given to the translation function and also returned 
   (appropriately updated) in the result. In the case above the
   input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
@@ -49,12 +49,12 @@
   An index is also produced whenever the translation
   function cannot find an appropriate propositional formula for a term. 
   Attempting to translate @{term "\<forall>x::nat. P x"}
-*}
+\<close>
 
-ML %grayML{*val (pform', table') = 
-       Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
+ML %grayML\<open>val (pform', table') = 
+       Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty\<close>
 
-text {*
+text \<open>
   returns @{ML "BoolVar 1" in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
@@ -71,11 +71,11 @@
   @{ML_response_fake [display,gray]
   "SAT_Solver.invoke_solver \"minisat\" pform"
   "SAT_Solver.SATISFIABLE assg"}
-*}
+\<close>
 
-text {*
+text \<open>
   determines that the formula @{ML pform} is satisfiable. If we inspect
-  the returned function @{text assg}
+  the returned function \<open>assg\<close>
 
   @{ML_response [display,gray]
 "let
@@ -85,7 +85,7 @@
 end"
   "(NONE, SOME true, NONE)"}
 
-  we obtain a possible assignment for the variables @{text "A"} an @{text "B"}
+  we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close>
   that makes the formula satisfiable. 
 
   Note that we invoked the SAT solver with the string @{text [quotes] auto}. 
@@ -95,13 +95,13 @@
 
   There are also two tactics that make use of SAT solvers. One 
   is the tactic @{ML sat_tac in SAT}. For example 
-*}
+\<close>
 
 lemma "True"
-apply(tactic {* SAT.sat_tac @{context} 1 *})
+apply(tactic \<open>SAT.sat_tac @{context} 1\<close>)
 done
 
-text {*
+text \<open>
   However, for proving anything more exciting using @{ML "sat_tac" in SAT} you 
   have to use a SAT solver that can produce a proof. The internal 
   one is not usuable for this. 
@@ -115,7 +115,7 @@
   "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
   implemented in @{ML_file "Pure/General/table.ML"}.  
   \end{readmore}
-*}
+\<close>
 
 
 end