| author | wenzelm |
| Sun, 18 Apr 2021 23:37:59 +0200 | |
| changeset 60223 | 740ebee5948b |
| parent 60219 | b697895d2cea |
| child 60224 | a111e8e03ac2 |
| permissions | -rw-r--r-- |
| wenzelm@60223 | 1 |
* WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE; |
| wenzelm@60216 | 2 |
|
| wenzelm@60219 | 3 |
* WN: eliminate "handle _ => ..." (essential for PIDE interaction): |
| wenzelm@60219 | 4 |
- either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation |
| wenzelm@60219 | 5 |
- or more basic try/can combinators; |
| wenzelm@60216 | 6 |
|
| wenzelm@60219 | 7 |
* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real; |
| wenzelm@60219 | 8 |
|
| wenzelm@60216 | 9 |
* WN: eliminate numerals_to_free, use existing Isabelle/HOL facilities; |
| wenzelm@60216 | 10 |
|
| wenzelm@60216 | 11 |
* MW: clarify/eliminate Isabelle/Scala add-ons (presently unused) |
| wenzelm@60216 | 12 |
|
| wenzelm@60216 | 13 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars |
| wenzelm@60216 | 14 |
11a12 |
| wenzelm@60216 | 15 |
> src/Tools/isac/BridgeJEdit/isac.scala |
| wenzelm@60216 | 16 |
|
| wenzelm@60216 | 17 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala |
| wenzelm@60216 | 18 |
76a77 |
| wenzelm@60216 | 19 |
> "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
|
| wenzelm@60216 | 20 |
|
| wenzelm@60216 | 21 |
* clarify test of sym_thm (and variations): |
| wenzelm@60216 | 22 |
|
| wenzelm@60216 | 23 |
changeset: 60213:8b135961eb45 |
| wenzelm@60216 | 24 |
parent: 60211:b69ff7aee3f4 |
| wenzelm@60216 | 25 |
user: Walther Neuper <walther.neuper@jku.at> |
| wenzelm@60216 | 26 |
date: Sun Apr 18 15:19:32 2021 +0200 |
| wenzelm@60216 | 27 |
files: test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml test/Tools/isac/MathEngBasic/thmC.sml |
| wenzelm@60216 | 28 |
description: |
| wenzelm@60216 | 29 |
shift test without correction of error |