diff -r be23597e81db -r f875a25aa72d ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri May 17 10:38:01 2019 +0200
@@ -108,20 +108,20 @@
   of @{term even} and @{term odd}
 
   @{ML_matchresult [display,gray]
-"let
+\<open>let
   val input = filtered_input
-     (\"even and odd \" ^  
-      \"where \" ^
-      \"  even0[intro]: \\\"even 0\\\" \" ^ 
-      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
-      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
+     ("even and odd " ^  
+      "where " ^
+      "  even0[intro]: \"even 0\" " ^ 
+      "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^ 
+      "| oddS[intro]:  \"even n \<Longrightarrow> odd (Suc n)\" ")
 in
   parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
      [((even0,_), _),
       ((evenS,_), _),
-      ((oddS,_), _)]), [])"}
+      ((oddS,_), _)]), [])\<close>}
 
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we