Walther Neuper <neuper@ist.tugraz.at> [Sun, 19 May 2013 08:51:27 +0200] rev 48862
GCD_Poly_FP.thy improved with nat as much as possible instead int
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 May 2013 12:08:14 +0200] rev 48861
intermed. GCD_Poly_FP.thy termination
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 May 2013 10:47:23 +0200] rev 48860
GCD_Poly_FP.thy finished for univariate case
# 2 reasons for gcd_up not working are not resolved and marked with (*?FLORIAN*)
# strange observation: the not working version of dvd_up in 3cf89adce552
does not require the lemmata, but succeeds 'by pat_completenes auto'
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 May 2013 10:22:39 +0200] rev 48859
gcd_up works again
results of investigation will follow in subsequent commits
Walther Neuper <neuper@ist.tugraz.at> [Thu, 09 May 2013 17:04:01 +0200] rev 48858
before backtracing to working gcd_up
working gcd_up is a4ab6a2763c1.
also noted:
dvd_up now fast 'by pat_completeness auto' --
reasons might relate to reasons, why gcd_up does NOT work.
Walther Neuper <neuper@ist.tugraz.at> [Tue, 07 May 2013 12:22:07 +0200] rev 48857
polish GCD_Poly.thy
gcd_up doesn't work due to re-def. of lcoeff_up etc.
previous changeset a4ab6a2763c1 works.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 06 May 2013 19:14:35 +0200] rev 48856
tuned
Walther Neuper <neuper@ist.tugraz.at> [Mon, 06 May 2013 18:21:10 +0200] rev 48855
GCD_Poly_FP.thy code for univariate case finished
polished code made congruent to GCD_Poly.thy
termination proofs all missing
Walther Neuper <neuper@ist.tugraz.at> [Wed, 01 May 2013 11:59:33 +0200] rev 48854
tuned
Walther Neuper <neuper@ist.tugraz.at> [Wed, 01 May 2013 11:52:37 +0200] rev 48853
GCD_Poly.thy tuned
add and mult of poly with map, fold
dvd and div not tried