1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TODO.md	Sun Apr 18 16:30:11 2021 +0200
     1.3 @@ -0,0 +1,36 @@
     1.4 +* switch `isa` repository to Isabelle repository clone (instead of Isabelle2021 release)
     1.5 +  * MW: remove clones of Isabelle2021 and refer to separate Isabelle repos instead;
     1.6 +  * MW: proper build Isabelle/Scala add-ons (presently unused);
     1.7 +
     1.8 +* Isabelle/ML brush-up:
     1.9 +  * MW: provide @{isac_test ML} antiquotation, based on system option "isac_test";
    1.10 +  * WN: clean up meta-comments for testing (remove or upgrade to @{isac_test});
    1.11 +  * WN: eliminate "handle _ => ..." , either use @{try} / @{can} antiquotation
    1.12 +    or more basic try/can combinators;
    1.13 +
    1.14 +* systematic test runs, as regular Isabelle build session
    1.15 +  * eliminate xcoding-to-test.sh etc.;
    1.16 +  * proper ROOT for all tests: `Test_Isac_Short`;
    1.17 +
    1.18 +* MW: eliminate odd notation term tricks, e.g. "^^^";
    1.19 +* WN: eliminate numerals_to_free, use existing Isabelle/HOL facilities;
    1.20 +
    1.21 +* MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
    1.22 +
    1.23 +    diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
    1.24 +    11a12
    1.25 +    >   src/Tools/isac/BridgeJEdit/isac.scala
    1.26 +
    1.27 +    diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala
    1.28 +    76a77
    1.29 +    >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
    1.30 +
    1.31 +* clarify test of sym_thm (and variations):
    1.32 +
    1.33 +changeset:   60213:8b135961eb45
    1.34 +parent:      60211:b69ff7aee3f4
    1.35 +user:        Walther Neuper <walther.neuper@jku.at>
    1.36 +date:        Sun Apr 18 15:19:32 2021 +0200
    1.37 +files:       test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml test/Tools/isac/MathEngBasic/thmC.sml
    1.38 +description:
    1.39 +shift test without correction of error