1 * WN: clean up meta-comments for testing:
2 - use \<^isac_test>CARTOUCHE for signature and structure body where actually required;
3 - remove vacous comments;
5 * WN or MW: remove eliminate xcoding-to-test.sh etc. --- option "isac_test" takes over this role
6 (already present in $ISABELLE_ISAC_TEST/ROOT)
8 * WN: eliminate "handle _ => ..." (essential for PIDE interaction):
9 - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
10 - or more basic try/can combinators;
12 * WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real;
14 * WN: eliminate numerals_to_free, use existing Isabelle/HOL facilities;
16 * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
18 diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
20 > src/Tools/isac/BridgeJEdit/isac.scala
22 diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala
24 > "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
26 * clarify test of sym_thm (and variations):
28 changeset: 60213:8b135961eb45
29 parent: 60211:b69ff7aee3f4
30 user: Walther Neuper <walther.neuper@jku.at>
31 date: Sun Apr 18 15:19:32 2021 +0200
32 files: test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml test/Tools/isac/MathEngBasic/thmC.sml
34 shift test without correction of error