1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri May 24 14:25:34 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri May 24 16:50:31 2013 +0200
     1.3 @@ -728,7 +728,6 @@
     1.4       yields  new_g = [1] \<or> (new_g \<ge> g \<and> P > M)
     1.5  
     1.6    argumentns "a b d M P g p" named according to [1] p.93: "p" is "prime", not "poly" ! *)
     1.7 -(*declare [[show_types]]*)
     1.8  function try_new_prime_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unipoly \<Rightarrow> nat \<Rightarrow> unipoly" 
     1.9  where 
    1.10  "try_new_prime_up             a          b          d      M      P     g          p   = 
    1.11 @@ -747,8 +746,7 @@
    1.12          let 
    1.13            P = P * p;
    1.14            g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
    1.15 -        in
    1.16 -          try_new_prime_up a b d M P g p)"
    1.17 +        in try_new_prime_up a b d M P g p)"
    1.18  by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
    1.19  termination try_new_prime_up (*by lexicographic_order LOOPS +PROOF:? / by size_change LOOPS*)
    1.20  (*apply (relation "measures