1.1 --- a/src/Tools/isac/TODO.thy	Fri Apr 17 18:47:29 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Sun Apr 19 11:07:02 2020 +0200
     1.3 @@ -50,19 +50,13 @@
     1.4  \<close>
     1.5  subsection \<open>Postponed from current changeset\<close>
     1.6  text \<open>
     1.7 -  \item "TODO CLEANUP Thm"
     1.8 -    (* TODO CLEANUP Thm:
     1.9 -    Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
    1.10 -    thmID            : type for data from user input + program
    1.11 -    thmDeriv         : type for thy_hierarchy ONLY
    1.12 -    obsolete types   : thm' (SEE "ad thm'"), thm''. 
    1.13 -    revise funs      : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
    1.14 -    activate         : ThmC.cut_id'
    1.15 -    *)
    1.16 +  \begin{itemize}
    1.17 +  \item xxx
    1.18 +  \item xxx
    1.19    \item xxx
    1.20    \item use "Exec_Def" for renaming identifiers
    1.21    \item xxx
    1.22 -  \item xxx
    1.23 +  \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
    1.24    \item xxx
    1.25    \item xxx
    1.26    \begin{itemize}
    1.27 @@ -610,6 +604,33 @@
    1.28  \begin{itemize}
    1.29  \item ad ERROR Undefined fact "all_left"        in Test_Isac: error-pattern.sml
    1.30                 Undefined fact: "xfoldr_Nil"                   inssort.sml
    1.31 +    (* probably two different reasons:
    1.32 +    src/../LinEq.thy
    1.33 +      (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
    1.34 +      all_left:          "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
    1.35 +    
    1.36 +    src/../PolyEq.thy
    1.37 +      (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
    1.38 +      all_left:              "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
    1.39 +    
    1.40 +    test/../partial_fractions.sml
    1.41 +    (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
    1.42 +    (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
    1.43 +    
    1.44 +    test/../mathengine-stateless.sml
    1.45 +    (*if ThmC.string_of_thm @ {thm rnorm_equation_add} =  "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
    1.46 +    then () else error "string_of_thm changed";*)
    1.47 +    
    1.48 +    (*---------------------------------------------------------------------------------------------*)
    1.49 +    src/../LinEq.thy
    1.50 +    primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.51 +    xfoldr_Nil:  "xfoldr f {|| ||} = id" |
    1.52 +    xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
    1.53 +    
    1.54 +    src/../InsSort.thy
    1.55 +        srls = Rule_Set.empty, calc = [], rules = [
    1.56 +          Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
    1.57 +    *)
    1.58  \item xxx
    1.59  \item xxx
    1.60  \item ?OK Test_Isac_Short with