1.1 --- a/TODO.md	Mon Apr 19 15:48:46 2021 +0200
     1.2 +++ b/TODO.md	Mon Apr 19 18:04:48 2021 +0200
     1.3 @@ -1,12 +1,29 @@
     1.4 -* WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
     1.5 -
     1.6  * WN: eliminate "handle _ => ..." (essential for PIDE interaction):
     1.7      - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
     1.8      - or more basic try/can combinators;
     1.9 +    - or more direct ML of intention;
    1.10  
    1.11 -* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real;
    1.12 +* WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
    1.13  
    1.14 -* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation;
    1.15 +* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>"
    1.16 +  based on "_ powr _" for type real;
    1.17 +
    1.18 +    abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.19 +      where "x \<up> a \<equiv> x powr a"
    1.20 +
    1.21 +* WN: purge BridgeLibisabelle: eliminate unused code;
    1.22 +
    1.23 +
    1.24 +* reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
    1.25 +
    1.26 +
    1.27 +* MW: clarify isac_test within theory Isac_Test.Isac_Test_Short;
    1.28 +* MW: check JVM resource requirements of session Isac_Test;
    1.29 +
    1.30 +* MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.31 +
    1.32 +* MW: proper formal name space for rule set, model patterns, methods;
    1.33 +  proper setup command;
    1.34  
    1.35  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
    1.36  
    1.37 @@ -18,6 +35,7 @@
    1.38      76a77
    1.39      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
    1.40  
    1.41 -* reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
    1.42  
    1.43 -* MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.44 +* more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations;
    1.45 +
    1.46 +* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation;