Walther Neuper <neuper@ist.tugraz.at> [Mon, 02 Sep 2013 15:17:34 +0200] rev 52100
GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy
Walther Neuper <neuper@ist.tugraz.at> [Mon, 02 Sep 2013 14:56:57 +0200] rev 52099
GCD_Poly_ML: generalised gcd_poly handling monomials
this also fixes bug in 6ceee9c5d6fd, which had been fixed in bb49dd92fa04 half-assed.
Walther Neuper <neuper@ist.tugraz.at> [Sun, 01 Sep 2013 16:50:51 +0200] rev 52098
GCD_Poly_ML: removed bug in gcd_poly when applied to two monomials
Walther Neuper <neuper@ist.tugraz.at> [Sun, 01 Sep 2013 15:54:48 +0200] rev 52097
GCD_Poly_ML: bug in gcd_poly when applied to two monomials
Walther Neuper <neuper@ist.tugraz.at> [Fri, 30 Aug 2013 13:43:30 +0200] rev 52096
GCD_Poly_ML: rewrite cancel is NONE if gcd_poly is 1
Walther Neuper <neuper@ist.tugraz.at> [Wed, 28 Aug 2013 11:48:37 +0200] rev 52095
GCD_Poly_ML: test 2nd level integration of gcd_poly
test --- and app_rev --- shows the respective part of the rewriter
Walther Neuper <neuper@ist.tugraz.at> [Wed, 28 Aug 2013 11:02:03 +0200] rev 52094
GCD_Poly_ML: correct & improve assumptions generated from gcd_pol
Walther Neuper <neuper@ist.tugraz.at> [Wed, 28 Aug 2013 10:40:53 +0200] rev 52093
GCD_Poly_ML: test 1st level integration of gcd_poly
Walther Neuper <neuper@ist.tugraz.at> [Mon, 26 Aug 2013 16:32:21 +0200] rev 52092
tuned
Walther Neuper <neuper@ist.tugraz.at> [Mon, 26 Aug 2013 15:37:48 +0200] rev 52091
GCD_Poly_ML: integrated gcd_poly into Rational.thy
replaced exactly fun factout_p_, fun cancel_p_, fun common_nominator_p_, fun add_fraction_p_
and left the other old code in the file in order to find out further functions still required.
Test_Isac.thy works except "exception- Size raised" in solve.sml,
polyeq.sml is out commented (but works if evaluated in two pieces).