# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1369304942 -7200
# Node ID 22948dd96b4259b73554edfdc7d9a1f8a362a0b2
# Parent  97408b42129d1a18f5fb61d040c37571f29568ee
tuned

diff -r 97408b42129d -r 22948dd96b42 src/Tools/isac/Knowledge/GCD_Poly.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Thu May 23 12:20:28 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Thu May 23 12:29:02 2013 +0200
@@ -90,8 +90,8 @@
   fun a div2 b = 
     if a div b < 0 then (abs a) div (abs b) * ~1 else a div b
 
-  (* why has this been removed since 2002 ? *)
-  fun last_elem ls = (hd o rev) ls
+  (* why has "last" been removed since 2002, although "last" is in List.thy ? *)
+  fun last ls = (hd o rev) ls
 
   (* drop tail elements equal 0 *)
   fun drop_hd_zeros (0 :: ps) = drop_hd_zeros ps
@@ -159,7 +159,7 @@
      yields n \<le> maxs pps  \<and>  (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p)  \<and>
        (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*)
     fun make_primes ps last_p n =
-        if n <= last_elem ps then ps else
+        if n <= last ps then ps else
           if is_prime ps (last_p + 2) 
           then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n
           else make_primes  ps                   (last_p + 2) n
@@ -191,7 +191,7 @@
 subsection {* basic notions for univariate polynomials *}
 ML {*
   (* leading coefficient, includes drop_lc0_up ?FIXME130507 *)
-  fun lcoeff_up (p: unipoly) = (last_elem o drop_tl_zeros) p
+  fun lcoeff_up (p: unipoly) = (last o drop_tl_zeros) p
   
   (* drop leading coefficients equal 0 *)
   fun drop_lc0_up (p: unipoly) = drop_tl_zeros p : unipoly;
@@ -452,13 +452,13 @@
   fun  lex_ord ((_, a): monom) ((_, b): monom) =
     let val d = drop_tl_zeros (a %-% b)
     in
-      if d = [] then false else last_elem d > 0
+      if d = [] then false else last d > 0
     end
   fun  lex_ord' ((_, a): monom, (_, b): monom) =
     let val d = drop_tl_zeros (a %-% b)
     in
       if  d = [] then EQUAL 
-      else if last_elem d > 0 then GREATER else LESS
+      else if last d > 0 then GREATER else LESS
     end
 
   (* add monomials in ordered polynomal *)
@@ -650,7 +650,7 @@
      | next_step steps new_steps x =  
        next_step (tl steps)
          (new_steps @ 
-           [((last_elem new_steps) %%-%% (hd steps)) %%/ ((last_elem x) - (nth x (length x - 3)))])
+           [((last new_steps) %%-%% (hd steps)) %%/ ((last x) - (nth x (length x - 3)))])
          (nth_drop (length x -2) x)
 
   fun NEWTON x f (steps: poly list) (up: unipoly) (p: poly) ord = 
@@ -663,9 +663,9 @@
         val new_vals = 
           multi_to_uni ((uni_to_multi up) %%*%% (uni_to_multi [(nth x (length x -2) ) * ~1, 1]));
         val new_steps = [((nth f (length f - 1)) %%-%% (nth f (length f - 2))) %%/ 
-          ((last_elem x) - (nth x (length x - 2)))];
+          ((last x) - (nth x (length x - 2)))];
         val steps = next_step steps new_steps x;
-        val p' = p %%+%% (mult_with_new_var (last_elem steps) new_vals ord);
+        val p' = p %%+%% (mult_with_new_var (last steps) new_vals ord);
       in (order p', new_vals, steps) end 
 *}