finished demo for Coimbra
authorWalther Neuper <neuper@ist.tugraz.at>
Wed, 23 Jul 2014 14:09:51 +0200
changeset 554755fcb9794169d
parent 55474 ac8d8d15b9dc
child 55476 8e3f73e1e3a3
finished demo for Coimbra
src/Tools/isac/Knowledge/GCD_Poly_ML.thy
     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 {*