1.1 --- a/TODO.md	Tue Aug 10 10:27:15 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 11:01:18 2021 +0200
     1.3 @@ -53,9 +53,6 @@
     1.4  
     1.5  * WN: Avoid Thm.get_name_hint --- somewhat fragile.
     1.6  
     1.7 -* WN: eliminate ThyC.to_ctxt, use Proof_Context.init_global inline to make more
     1.8 -  clear where the normal Isabelle context-discipline is bypassed;
     1.9 -
    1.10  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.11      - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.12        without further ado;
    1.13 @@ -79,6 +76,6 @@
    1.14    + 0d22a6bf1fc6 was too much for 1 changeset
    1.15    + first parse with ctxt in Specify (O_Model.init shall return a context,..) etc
    1.16  
    1.17 -* WN: push initiatives of MW through the whole code
    1.18 -  + e1da148725ed : \<^ML>\<open>...\<close> instead parentheses
    1.19 +* WN: push suggestions of MW through the whole code
    1.20 +  + e1da148725ed : \<^ML>\<open>...\<close> instead of parentheses
    1.21    + 
    1.22 \ No newline at end of file