Walther Neuper <neuper@ist.tugraz.at> [Thu, 25 Apr 2013 13:58:36 +0200] rev 48849
polish GCD_Poly.thy: lex_ord interm.
Walther Neuper <neuper@ist.tugraz.at> [Sat, 20 Apr 2013 18:18:06 +0200] rev 48848
polish GCD_Poly.thy: lmonom done
Walther Neuper <neuper@ist.tugraz.at> [Sat, 20 Apr 2013 15:01:16 +0200] rev 48847
polish GCD_Poly.thy: lcoeff
Walther Neuper <neuper@ist.tugraz.at> [Fri, 12 Apr 2013 20:46:58 +0200] rev 48846
polished GCD_Poly.thy
still lots to do in multivariate code
Walther Neuper <neuper@ist.tugraz.at> [Fri, 12 Apr 2013 11:03:41 +0200] rev 48845
before finalizing GCD_Poly.thy
Walther Neuper <neuper@ist.tugraz.at> [Thu, 21 Mar 2013 15:40:13 +0100] rev 48844
GCD_Poly ML-->Isabelle: simplified dvd for univariate polynomials
this simplification (tested in gcd_poly.sml)
simplifies proof for pattern compatibility.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 18 Mar 2013 10:46:55 +0100] rev 48843
merged
Walther Neuper <neuper@ist.tugraz.at> [Mon, 18 Mar 2013 10:46:37 +0100] rev 48842
GCD_Poly ML-->Isabelle: intermediate
diana <meindl_diana@yahoo.com> [Sat, 16 Mar 2013 14:52:02 +0100] rev 48841
GCD_POLY -> new fun %%/%%
Walther Neuper <neuper@ist.tugraz.at> [Wed, 06 Mar 2013 09:43:41 +0100] rev 48840
merged