equal
deleted
inserted
replaced
33 * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c"; |
33 * WN: clarify add_calcs with non-existant constant "Integrate.add_new_c"; |
34 |
34 |
35 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations, |
35 * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations, |
36 e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try"; |
36 e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try"; |
37 |
37 |
38 * WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"): |
|
39 Is this really required, or can we just use the 'method' command? |
|
40 |
|
41 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by |
38 * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by |
42 ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close> |
39 ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close> |
43 |
40 |
44 * WN: Avoid Thm.get_name_hint --- somewhat fragile. |
41 * WN: Avoid Thm.get_name_hint --- somewhat fragile. |
45 |
42 |