author | Walther Neuper <neuper@ist.tugraz.at> |
Wed, 23 Jul 2014 14:09:51 +0200 | |
changeset 55475 | 5fcb9794169d |
parent 55474 | ac8d8d15b9dc |
child 55476 | 8e3f73e1e3a3 |
1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Thu Jul 03 13:43:12 2014 +0200 1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Wed Jul 23 14:09:51 2014 +0200 1.3 @@ -1354,8 +1354,10 @@ 1.4 ML {* 1.5 trace_Euclid := true; 1.6 trace_div_invariant := false; 1.7 + trace_div := false; 1.8 EUCLID_naive_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] 1.9 *} 1.10 +thm gcd_add_mult_int 1.11 1.12 subsection {* Step-wise Construction of DIV and GCD *} 1.13 text {*