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