Walther Neuper <neuper@ist.tugraz.at> [Fri, 13 Sep 2013 18:57:11 +0200] rev 52102
Test_Theory without session Isac has limitations
Walther Neuper <neuper@ist.tugraz.at> [Mon, 02 Sep 2013 16:16:08 +0200] rev 52101
Test_Isac works again, almost ..
4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"
The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82.
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