(* Title:  todo's for isac core

    Author: Walther Neuper 111013

    (c) copyright due to lincense terms.

 *)

 theory TODO

 imports "~~/src/Doc/Prog_Prove/LaTeXsugar"

 begin

 section \<open>TODOs from current development\<close>

 subsection \<open>Shift programs for Lucas-Interpretation from strings to partial_function\<close>

 text\<open>

 String constants have already bee introduced to old string-programs.

 Shifting this program code into partial_function reveals further issues:

 \begin{itemize}

 \item Diff.thy

   \begin{itemize}

   \item differentiateX --> differentiate after removal of script-constant

   \end{itemize}

 \item Inverse_Z_Transform.thy: thm ruleZY introduces a new variable on the rhs of the rewrite-rule.

   The problem is related to the decision of typing for "d_d" and making bound variables free (while

   shifting specific handling in equation solving etc. to the metalogic.

 \item Test.thy: met_test_sqrt2: deleted?!

 \item 

   \begin{itemize}

   \item 

   \end{itemize}

 \end{itemize}

 \<close>

 subsubsection \<open>\<close>

 section \<open>TODOs shifted here from above\<close>

 subsection \<open>adopt Isabelle's numerals for Isac\<close>

 text \<open>WN131021: 

 intermediate states:

 # replace numerals of type "real" by "nat" in some specific functions from ListC.thy

   and have both representations in parallel for "nat".

 \<close>subsection \<open>finetunig required for xmldata\<close>

 text \<open>WN140808: 

 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390

 and in kbase html-representation generated from these xmldata.

 Notes in ~~/xmldata/TODO.txt.

 \<close>

 section \<open>\<close>

 subsection \<open>\<close>

 subsubsection \<open>\<close>

 text\<open>

 \begin{itemize}

 \item 

 \end{itemize}

 \<close>

 end