1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -10,12 +10,12 @@
     1.4  ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
     1.5  ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
     1.6  ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
     1.7 -ML {*
     1.8 -*} ML {*
     1.9 -*} 
    1.10 +ML \<open>
    1.11 +\<close> ML \<open>
    1.12 +\<close> 
    1.13  
    1.14 -subsection {* Notes on Isac's programming language *}
    1.15 -text {*
    1.16 +subsection \<open>Notes on Isac's programming language\<close>
    1.17 +text \<open>
    1.18    Isac's programming language combines tacticals (TRY, etc) and 
    1.19    tactics (Rewrite, etc) with list processing.
    1.20  
    1.21 @@ -37,9 +37,9 @@
    1.22  
    1.23    Note: *one* "axiomatization" over all equations caused strange "'a list list"
    1.24    types.
    1.25 -*}
    1.26 +\<close>
    1.27  
    1.28 -subsection {* Type 'xlist' for Lucas-Interpretation *}
    1.29 +subsection \<open>Type 'xlist' for Lucas-Interpretation\<close>
    1.30  (* cp fom ~~/src/HOL/List.thy
    1.31     TODO: ask for shorter deliminters in xlist *)
    1.32  datatype  'a xlist =
    1.33 @@ -57,7 +57,7 @@
    1.34  term "{|| ||}"
    1.35  term "{||1,2,3||}"
    1.36  
    1.37 -subsection {* Functions for 'xlist' *}
    1.38 +subsection \<open>Functions for 'xlist'\<close>
    1.39  (* TODO: 
    1.40  (1) revise, if definition of identifiers like LENGTH_NIL are still required.
    1.41  (2) switch the role of 'xlist' and 'list' in the functions below, in particular for
    1.42 @@ -132,7 +132,7 @@
    1.43  
    1.44  (** Lexicographic orderings on lists ...!!!**)
    1.45  
    1.46 -ML{* (*the former ListC.ML*)
    1.47 +ML\<open>(*the former ListC.ML*)
    1.48  (** rule set for evaluating listexpr in scripts **)
    1.49  val list_rls = 
    1.50    Rule.Rls {id = "list_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 
    1.51 @@ -181,7 +181,7 @@
    1.52         Rule.Thm ("zip_Cons",TermC.num_str @{thm zip_Cons}),
    1.53         Rule.Thm ("zip_Nil",TermC.num_str @{thm zip_Nil})],
    1.54      scr = Rule.EmptyScr}: Rule.rls;
    1.55 -*}
    1.56 -setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
    1.57 +\<close>
    1.58 +setup \<open>KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))]\<close>
    1.59  
    1.60  end