1.1 --- a/TODO.md Mon Jun 21 15:42:53 2021 +0200
1.2 +++ b/TODO.md Mon Jun 21 15:50:58 2021 +0200
1.3 @@ -27,18 +27,21 @@
1.4 * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
1.5
1.6
1.7 +* WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
1.8 + e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
1.9 +
1.10 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
1.11 - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
1.12
1.13 +* WN: proper formal context with theory HOL-Library.Float, proper antiquotation @{const_name Float};
1.14 +
1.15 * WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
1.16
1.17 * WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
1.18 Is this really required, or can we just use the 'method' command?
1.19
1.20 -* WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
1.21 - (following the "TODO" comment);
1.22 -
1.23 -* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed.
1.24 +* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed;
1.25 + improve errors via parse_term_strict;
1.26
1.27 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
1.28