Walther Neuper <neuper@ist.tugraz.at> [Tue, 17 Sep 2013 09:50:52 +0200] rev 52107
separated Isac documentation (~~/doc-isac) from Isabelle documentation (~~/src/Doc)
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Sep 2013 12:27:20 +0200] rev 52106
review of examples for non-termination of rls norm_Rational
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Sep 2013 12:20:00 +0200] rev 52105
Test_Isac works again, perfectly ..
# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}.
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Sep 2013 11:28:43 +0200] rev 52104
gcd_poly requires special handling for a monomial argument
Walther Neuper <neuper@ist.tugraz.at> [Mon, 16 Sep 2013 10:46:51 +0200] rev 52103
tolerate Var in rewriting
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