Mon, 16 Sep 2013 10:46:51 +0200tolerate Var in rewriting
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Sep 2013 10:46:51 +0200] rev 52103
tolerate Var in rewriting

Fri, 13 Sep 2013 18:57:11 +0200Test_Theory without session Isac has limitations
Walther Neuper <neuper@ist.tugraz.at> [Fri, 13 Sep 2013 18:57:11 +0200] rev 52102
Test_Theory without session Isac has limitations

Mon, 02 Sep 2013 16:16:08 +0200Test_Isac works again, almost ..
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.

Mon, 02 Sep 2013 15:17:34 +0200GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy
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

Mon, 02 Sep 2013 14:56:57 +0200GCD_Poly_ML: generalised gcd_poly handling monomials
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.

Sun, 01 Sep 2013 16:50:51 +0200GCD_Poly_ML: removed bug in gcd_poly when applied to two monomials
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

Sun, 01 Sep 2013 15:54:48 +0200GCD_Poly_ML: 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

Fri, 30 Aug 2013 13:43:30 +0200GCD_Poly_ML: rewrite cancel is NONE if gcd_poly is 1
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

Wed, 28 Aug 2013 11:48:37 +0200GCD_Poly_ML: test 2nd level integration of gcd_poly
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

Wed, 28 Aug 2013 11:02:03 +0200GCD_Poly_ML: correct & improve assumptions generated from gcd_pol
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