1.1 --- a/TODO.md	Tue Apr 20 23:20:45 2021 +0200
     1.2 +++ b/TODO.md	Wed Apr 21 10:09:14 2021 +0200
     1.3 @@ -5,12 +5,6 @@
     1.4  
     1.5  * WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
     1.6  
     1.7 -* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>"
     1.8 -  based on "_ powr _" for type real;
     1.9 -
    1.10 -    abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.11 -      where "x \<up> a \<equiv> x powr a"
    1.12 -
    1.13  * WN: purge BridgeLibisabelle: eliminate unused code;
    1.14  
    1.15  
    1.16 @@ -45,6 +39,8 @@
    1.17      - sometimes this requires to use more specific types / type classes;
    1.18      - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun');
    1.19      - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation);
    1.20 +    - abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real"  (infixr "\<up>" 80)
    1.21 +      where "x \<up> a \<equiv> x powr a"
    1.22  
    1.23  * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
    1.24      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");