1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Thu May 23 12:20:28 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Thu May 23 12:29:02 2013 +0200
     1.3 @@ -90,8 +90,8 @@
     1.4    fun a div2 b = 
     1.5      if a div b < 0 then (abs a) div (abs b) * ~1 else a div b
     1.6  
     1.7 -  (* why has this been removed since 2002 ? *)
     1.8 -  fun last_elem ls = (hd o rev) ls
     1.9 +  (* why has "last" been removed since 2002, although "last" is in List.thy ? *)
    1.10 +  fun last ls = (hd o rev) ls
    1.11  
    1.12    (* drop tail elements equal 0 *)
    1.13    fun drop_hd_zeros (0 :: ps) = drop_hd_zeros ps
    1.14 @@ -159,7 +159,7 @@
    1.15       yields n \<le> maxs pps  \<and>  (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p)  \<and>
    1.16         (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*)
    1.17      fun make_primes ps last_p n =
    1.18 -        if n <= last_elem ps then ps else
    1.19 +        if n <= last ps then ps else
    1.20            if is_prime ps (last_p + 2) 
    1.21            then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n
    1.22            else make_primes  ps                   (last_p + 2) n
    1.23 @@ -191,7 +191,7 @@
    1.24  subsection {* basic notions for univariate polynomials *}
    1.25  ML {*
    1.26    (* leading coefficient, includes drop_lc0_up ?FIXME130507 *)
    1.27 -  fun lcoeff_up (p: unipoly) = (last_elem o drop_tl_zeros) p
    1.28 +  fun lcoeff_up (p: unipoly) = (last o drop_tl_zeros) p
    1.29    
    1.30    (* drop leading coefficients equal 0 *)
    1.31    fun drop_lc0_up (p: unipoly) = drop_tl_zeros p : unipoly;
    1.32 @@ -452,13 +452,13 @@
    1.33    fun  lex_ord ((_, a): monom) ((_, b): monom) =
    1.34      let val d = drop_tl_zeros (a %-% b)
    1.35      in
    1.36 -      if d = [] then false else last_elem d > 0
    1.37 +      if d = [] then false else last d > 0
    1.38      end
    1.39    fun  lex_ord' ((_, a): monom, (_, b): monom) =
    1.40      let val d = drop_tl_zeros (a %-% b)
    1.41      in
    1.42        if  d = [] then EQUAL 
    1.43 -      else if last_elem d > 0 then GREATER else LESS
    1.44 +      else if last d > 0 then GREATER else LESS
    1.45      end
    1.46  
    1.47    (* add monomials in ordered polynomal *)
    1.48 @@ -650,7 +650,7 @@
    1.49       | next_step steps new_steps x =  
    1.50         next_step (tl steps)
    1.51           (new_steps @ 
    1.52 -           [((last_elem new_steps) %%-%% (hd steps)) %%/ ((last_elem x) - (nth x (length x - 3)))])
    1.53 +           [((last new_steps) %%-%% (hd steps)) %%/ ((last x) - (nth x (length x - 3)))])
    1.54           (nth_drop (length x -2) x)
    1.55  
    1.56    fun NEWTON x f (steps: poly list) (up: unipoly) (p: poly) ord = 
    1.57 @@ -663,9 +663,9 @@
    1.58          val new_vals = 
    1.59            multi_to_uni ((uni_to_multi up) %%*%% (uni_to_multi [(nth x (length x -2) ) * ~1, 1]));
    1.60          val new_steps = [((nth f (length f - 1)) %%-%% (nth f (length f - 2))) %%/ 
    1.61 -          ((last_elem x) - (nth x (length x - 2)))];
    1.62 +          ((last x) - (nth x (length x - 2)))];
    1.63          val steps = next_step steps new_steps x;
    1.64 -        val p' = p %%+%% (mult_with_new_var (last_elem steps) new_vals ord);
    1.65 +        val p' = p %%+%% (mult_with_new_var (last steps) new_vals ord);
    1.66        in (order p', new_vals, steps) end 
    1.67  *}
    1.68