more TODO caused by ac7426ab0491
authorwneuper <walther.neuper@jku.at>
Tue, 20 Apr 2021 17:21:08 +0200
changeset 6024562d165c78123
parent 60244 ac7426ab0491
child 60246 2e30d48fcd0b
child 60248 2022f88eee80
more TODO caused by ac7426ab0491
TODO.md
     1.1 --- a/TODO.md	Tue Apr 20 17:10:02 2021 +0200
     1.2 +++ b/TODO.md	Tue Apr 20 17:21:08 2021 +0200
     1.3 @@ -44,3 +44,6 @@
     1.4  
     1.5  * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation
     1.6      - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float");
     1.7 +
     1.8 +* WN: investigate errors further which popped up in rewriting when replacing ^^^ by \<up> in ac7426ab0491.
     1.9 +      The errors occur with examples in test/../poly.sml, which do not work properly in isabisac20 either.
    1.10 \ No newline at end of file