wenzelm@60219
|
1 |
* WN: eliminate "handle _ => ..." (essential for PIDE interaction):
|
wenzelm@60219
|
2 |
- either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
|
wenzelm@60219
|
3 |
- or more basic try/can combinators;
|
wenzelm@60234
|
4 |
- or more direct ML of intention;
|
wenzelm@60216
|
5 |
|
wenzelm@60234
|
6 |
* WN: purge BridgeLibisabelle: eliminate unused code;
|
wenzelm@60234
|
7 |
|
wenzelm@60234
|
8 |
|
wenzelm@60234
|
9 |
* reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
|
wenzelm@60234
|
10 |
|
wenzelm@60234
|
11 |
|
wenzelm@60247
|
12 |
* MW: ML antiqutation @{rule_thm NAME} to produce (Rule.Thm ("NAME", ThmC.numerals_to_Free "NAME"));
|
wenzelm@60247
|
13 |
|
wenzelm@60247
|
14 |
* MW: more concise "setup KEStore_Elems.add_rlss" etc.;
|
wenzelm@60247
|
15 |
|
wenzelm@60234
|
16 |
* MW: check uses of Unsynchronized.ref vs. Synchronized.var;
|
wenzelm@60234
|
17 |
|
wenzelm@60234
|
18 |
* MW: proper formal name space for rule set, model patterns, methods;
|
wenzelm@60234
|
19 |
proper setup command;
|
wenzelm@60216
|
20 |
|
wenzelm@60216
|
21 |
* MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
|
wenzelm@60216
|
22 |
|
wenzelm@60216
|
23 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
|
wenzelm@60216
|
24 |
11a12
|
wenzelm@60216
|
25 |
> src/Tools/isac/BridgeJEdit/isac.scala
|
wenzelm@60216
|
26 |
|
wenzelm@60216
|
27 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala
|
wenzelm@60216
|
28 |
76a77
|
wenzelm@60216
|
29 |
> "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
|
wenzelm@60225
|
30 |
|
wenzelm@60229
|
31 |
|
wenzelm@60241
|
32 |
* WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
|
wenzelm@60241
|
33 |
- quite often "axiomatization ..." can be turned into "lemma ... by auto"
|
wenzelm@60241
|
34 |
without further ado;
|
wenzelm@60241
|
35 |
- sometimes this requires to use more specific types / type classes;
|
wenzelm@60241
|
36 |
- sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
|
wenzelm@60241
|
37 |
- a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
|
walther@60248
|
38 |
- abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80)
|
walther@60248
|
39 |
where "x \<up> a \<equiv> x powr a"
|
wenzelm@60234
|
40 |
|
wenzelm@60241
|
41 |
* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
|
wenzelm@60241
|
42 |
- clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
|
walther@60245
|
43 |
|
walther@60245
|
44 |
* WN: investigate errors further which popped up in rewriting when replacing ^^^ by \<up> in ac7426ab0491.
|
wenzelm@60247
|
45 |
The errors occur with examples in test/../poly.sml, which do not work properly in isabisac20 either.
|
wenzelm@60247
|
46 |
|
wenzelm@60247
|
47 |
* WN: cleanup remaining ^^^ in comments (but sometimes it is just ASCII art);
|
wenzelm@60247
|
48 |
|
wenzelm@60247
|
49 |
* WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
|
wenzelm@60247
|
50 |
|
wenzelm@60247
|
51 |
* WN: proper statement for rcancel_den ("not" is a free variable!?!!):
|
wenzelm@60247
|
52 |
rcancel_den: "not(a=0) ==> a * (b / a) = b" and
|
wenzelm@60247
|
53 |
|
wenzelm@60247
|
54 |
* WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
|
wenzelm@60247
|
55 |
|
wenzelm@60250
|
56 |
* WN: use File.read / File.write instead of low-level TextIO operations (not portable);
|
wenzelm@60250
|
57 |
* WN: use Path.T (e.g. via Path.explode) for portability;
|
wenzelm@60250
|
58 |
* WN: refrain from using global /tmp directory
|
wenzelm@60250
|
59 |
(e.g. see Isabelle_System.create_tmp_path / with_tmp_file / with_tmp_dir);
|