Walther Neuper <neuper@ist.tugraz.at> [Sat, 27 Apr 2013 12:27:38 +0200] rev 48852
tuned
Walther Neuper <neuper@ist.tugraz.at> [Sat, 27 Apr 2013 12:23:46 +0200] rev 48851
GCD_Poly.thy as submitted to Munich
TODOs:
# formal specifications for multivariate part
# normialise code with fold / map
# some renaming of identifiers
Walther Neuper <neuper@ist.tugraz.at> [Thu, 25 Apr 2013 18:49:52 +0200] rev 48850
polish GCD_Poly.thy: until gcd_poly'
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