1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Thu Feb 28 18:27:29 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Fri Mar 01 13:24:08 2019 +0100
     1.3 @@ -15,11 +15,9 @@
     1.4    KantenLaenge    :: "bool => una"
     1.5    Querschnitt     :: "bool => una"
     1.6    GesamtLaenge    :: "real => una"
     1.7 -(* version for later switch to partial_function
     1.8    oben            :: real
     1.9    senkrecht       :: real
    1.10    unten           :: real
    1.11 -*)
    1.12  
    1.13    (*Script-names*)
    1.14    RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
    1.15 @@ -58,17 +56,17 @@
    1.16  "symbolisch_rechnen k_k  q__q  u_u  s_s  o_o  l_l =
    1.17   (let t_t = Take (l_l = oben + senkrecht + unten);
    1.18      su_m = boollist2sum o_o;
    1.19 -    t_t = Substitute [oben = su_m] t_t;      \<comment> \<open>PROG consts\<close>
    1.20 +    t_t = Substitute [oben = su_m] t_t;
    1.21      t_t = Substitute o_o t_t;
    1.22      t_t = Substitute [k_k, q__q] t_t;
    1.23      t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
    1.24      su_m = boollist2sum s_s;
    1.25 -    t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
    1.26 +    t_t = Substitute [senkrecht = su_m] t_t;
    1.27      t_t = Substitute s_s t_t;
    1.28      t_t = Substitute [k_k, q__q] t_t;
    1.29      t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
    1.30      su_m = boollist2sum u_u;
    1.31 -    t_t = Substitute [unten = su_m] t_t;     \<comment> \<open>PROG consts\<close>
    1.32 +    t_t = Substitute [unten = su_m] t_t;
    1.33      t_t = Substitute u_u t_t;
    1.34      t_t = Substitute [k_k, q__q] t_t;
    1.35      t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t
    1.36 @@ -111,15 +109,15 @@
    1.37  (u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =
    1.38   (let t_t = Take (l_l = oben + senkrecht + unten);
    1.39        su_m = boollist2sum o_o;
    1.40 -      t_t = Substitute [oben = su_m] t_t;      \<comment> \<open>PROG consts\<close>
    1.41 +      t_t = Substitute [oben = su_m] t_t;
    1.42        t_t = Substitute o_o t_t;
    1.43        t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
    1.44        su_m = boollist2sum s_s;
    1.45 -      t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
    1.46 +      t_t = Substitute [senkrecht = su_m] t_t;
    1.47        t_t = Substitute s_s t_t;
    1.48        t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
    1.49        su_m = boollist2sum u_u;
    1.50 -      t_t = Substitute [unten = su_m] t_t;     \<comment> \<open>PROG consts\<close>
    1.51 +      t_t = Substitute [unten = su_m] t_t;
    1.52        t_t = Substitute u_u t_t;
    1.53        t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
    1.54        t_t = Substitute [k_k, q__q] t_t

     2.1 --- a/src/Tools/isac/TODO.thy	Thu Feb 28 18:27:29 2019 +0100
     2.2 +++ b/src/Tools/isac/TODO.thy	Fri Mar 01 13:24:08 2019 +0100
     2.3 @@ -14,7 +14,6 @@
     2.4  Shifting this program code into partial_function reveals further issues:
     2.5  \begin{itemize}
     2.6  \item "partial_function xxx .." introduces a constant "xxx" (see xxx.simps), might break tests
     2.7 -\item AlgEin.thy: oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
     2.8  \item Biegelinie.thy
     2.9    \begin{itemize}
    2.10    \item ?drop biegelinie_lang?

     3.1 --- a/test/Tools/isac/Knowledge/algein.sml	Thu Feb 28 18:27:29 2019 +0100
     3.2 +++ b/test/Tools/isac/Knowledge/algein.sml	Fri Mar 01 13:24:08 2019 +0100
     3.3 @@ -67,7 +67,7 @@
     3.4  val (p,_,f,nxt,_,pt) = me nxt p c pt(*Rewrite_Set "norm_Rational"*);f2str f;
     3.5  val (p,_,f,nxt,_,pt) = me nxt p c pt(**);
     3.6  if f2str f = "L = 32 + senkrecht + unten" then ()
     3.7 -else error "algein.sml diff.behav. in erstSymbolisch 1";
     3.8 +else error "algein.sml diff.behav. in erstNumerisch 1";
     3.9  val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
    3.10  val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
    3.11  val (p,_,f,nxt,_,pt) = me nxt p c pt;val(p,_,f,nxt,_,pt)=me nxt p c pt;f2str f;
    3.12 @@ -75,8 +75,8 @@
    3.13  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.14  if f2str f = "L = 104"
    3.15  then case nxt of ("End_Proof'", End_Proof') => ()
    3.16 -  | _ => error "algein.sml diff.behav. in erstSymbolisch 99 1"
    3.17 -else error "algein.sml diff.behav. in erstSymbolisch 99 2";
    3.18 +  | _ => error "algein.sml diff.behav. in erstNumerisch 99 1"
    3.19 +else error "algein.sml diff.behav. in erstNumerisch 99 2";
    3.20  DEconstrCalcTree 1;
    3.21  
    3.22  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";

     4.1 --- a/test/Tools/isac/Knowledge/poly.sml	Thu Feb 28 18:27:29 2019 +0100
     4.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Fri Mar 01 13:24:08 2019 +0100
     4.3 @@ -460,7 +460,7 @@
     4.4  "-------- norm_Poly NOT COMPLETE ------------------------";
     4.5  val SOME (f',_) = rewrite_set_ thy false norm_Poly 
     4.6  (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
     4.7 -if term2str f' = "L = 2 * 2 * k + oben + 2 * -4 * q + senkrecht"
     4.8 +if term2str f' = "L = 2 * 2 * k + 2 * -4 * q + senkrecht + oben"
     4.9  then ((*norm_Poly NOT COMPLETE -- TODO MG*))
    4.10  else error "norm_Poly changed behavior";
    4.11