1.1 --- a/TODO.md	Wed May 26 13:12:03 2021 +0200
     1.2 +++ b/TODO.md	Wed May 26 13:26:55 2021 +0200
     1.3 @@ -21,6 +21,15 @@
     1.4      76a77
     1.5      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
     1.6  
     1.7 +* MW: when Isabelle inner syntax is processed literally in Isabelle/ML, prefer formal Input.source
     1.8 +with literal \<open>...\<close> instead of old-fashioned "..."; this will eventually allow automated update of
     1.9 +old ASCII notation (e.g. "EX" vs. "\<exists>"), with the help of PIDE markup;
    1.10 +
    1.11 +
    1.12 +* What is the purpose of "#numeral" instead of plain numeral?
    1.13 +
    1.14 +* Check/clarify Context.theory_name vs. Context.theory_long_name.
    1.15 +
    1.16  
    1.17  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.18      - quite often "axiomatization ..." can be turned into "lemma ... by auto"