--- a/ProgTutorial/Solutions.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Wed May 22 12:38:51 2019 +0200
@@ -362,8 +362,10 @@
   This is all we need to let the conversion run against the simproc:
 \<close>
 
-ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
-val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)\<close>
+ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) 
+  (fn {context, ...} => c_tac context)
+val _ = Goal.prove @{context} [] [] (goal 8) 
+  (fn {context, ...} => s_tac context)\<close>
 
 text \<open>
   If you do the exercise, you can see that both ways of simplifying additions