27 without further ado; |
27 without further ado; |
28 - sometimes this requires to use more specific types / type classes; |
28 - sometimes this requires to use more specific types / type classes; |
29 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun'); |
29 - sometimes this requires to use proper definitional mechanisms (e.g. 'primrec', 'fun'); |
30 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation); |
30 - a few "hard" cases will remain, to be reconsidered eventually (e.g. differentiation); |
31 |
31 |
32 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation |
32 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation, DONE partially; |
33 - clarify role of type "real" vs. "float" (see theory "HOL-Library.Float"); |
33 - TODO: ? how to do algebraic operations on numerals ? Presburger ? simplifier ? |
|
34 - TODO: clarify role of type "real" vs. "float" (see theory "HOL-Library.Float"); |
34 |
35 |
35 * WN: Part.DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art); |
36 * WN: DONE cleanup remaining ^^^ in comments (but sometimes it is just ASCII art), partially; |
36 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too) |
37 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too) |
37 Left "ASCII art" in case of indicating comments pointing at facts ABOVE. |
38 Left "ASCII art" in case of indicating comments pointing at facts ABOVE. |
38 |
39 |
39 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing}; |
40 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing}; |
|
41 ??? |
|
42 |
|
43 * WN: reduce the number of TermC.parse*; |
|
44 - one or two variants should suffice. |