diff -r f2b3681fafb9 -r 3e904f8ec16c src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Wed Sep 05 18:09:56 2018 +0200
+++ b/src/Tools/isac/ProgLang/ListC.thy	Wed Nov 21 12:32:54 2018 +0100
@@ -10,12 +10,12 @@
 ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
 ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
 ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
-ML {*
-*} ML {*
-*} 
+ML \<open>
+\<close> ML \<open>
+\<close> 
 
-subsection {* Notes on Isac's programming language *}
-text {*
+subsection \<open>Notes on Isac's programming language\<close>
+text \<open>
   Isac's programming language combines tacticals (TRY, etc) and 
   tactics (Rewrite, etc) with list processing.
 
@@ -37,9 +37,9 @@
 
   Note: *one* "axiomatization" over all equations caused strange "'a list list"
   types.
-*}
+\<close>
 
-subsection {* Type 'xlist' for Lucas-Interpretation *}
+subsection \<open>Type 'xlist' for Lucas-Interpretation\<close>
 (* cp fom ~~/src/HOL/List.thy
    TODO: ask for shorter deliminters in xlist *)
 datatype  'a xlist =
@@ -57,7 +57,7 @@
 term "{|| ||}"
 term "{||1,2,3||}"
 
-subsection {* Functions for 'xlist' *}
+subsection \<open>Functions for 'xlist'\<close>
 (* TODO: 
 (1) revise, if definition of identifiers like LENGTH_NIL are still required.
 (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
@@ -132,7 +132,7 @@
 
 (** Lexicographic orderings on lists ...!!!**)
 
-ML{* (*the former ListC.ML*)
+ML\<open>(*the former ListC.ML*)
 (** rule set for evaluating listexpr in scripts **)
 val list_rls = 
   Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
@@ -181,7 +181,7 @@
        Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
        Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
     scr = Rule.EmptyScr}: Rule.rls;
-*}
-setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
+\<close>
+setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
 
 end