changeset 60363 | 66aa856ccf45 |
parent 60362 | de670839362e |
child 60364 | c76f66589c13 |
1.1 --- a/TODO.md Tue Aug 10 11:54:12 2021 +0200 1.2 +++ b/TODO.md Tue Aug 10 11:55:24 2021 +0200 1.3 @@ -12,7 +12,7 @@ 1.4 1.5 1.6 * Eliminate Thy_Info.get_theory eventually: should take theory from ancestory 1.7 - within current context. cf. e587c45cae0f note in Build_Thydata.thy 1.8 + within current context. 1.9 cf. e587c45cae0f note in Build_Thydata.thy 1.10 1.11 * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);