Walther Neuper <neuper@ist.tugraz.at> [Mon, 22 Jul 2013 14:09:26 +0200] rev 52071
started trials with Library/Polynomial.thy
Walther Neuper <neuper@ist.tugraz.at> [Mon, 22 Jul 2013 13:52:18 +0200] rev 52070
--- Test_Isac.thy runs all tests
NOTEs:
(1) inserted many "trace_rewrite := false" ...
(2) ...nevertheless needs manual interaction at "Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?"
(3) state of tests see respective section in Test_Isac.thy
Walther Neuper <neuper@ist.tugraz.at> [Sun, 21 Jul 2013 15:15:50 +0200] rev 52069
removed ERROR: Undefined session(s): "Isac"
Walther Neuper <neuper@ist.tugraz.at> [Sun, 21 Jul 2013 15:11:01 +0200] rev 52068
merged
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Jul 2013 14:31:58 +0200] rev 52067
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Jul 2013 14:30:58 +0200] rev 52066
tuned
Walther Neuper <neuper@ist.tugraz.at> [Sun, 21 Jul 2013 15:08:31 +0200] rev 52065
a bulky chunk of changes
# trials on GCD_Poly
# started to make Test_Isac.thy run
# new term2str
Walther Neuper <neuper@ist.tugraz.at> [Sat, 20 Jul 2013 08:07:39 +0200] rev 52064
hint for transition to Isabelle's numerals, cf. num_str
Walther Neuper <neuper@ist.tugraz.at> [Thu, 18 Jul 2013 14:26:49 +0200] rev 52063
GCD_Poly trials with naive Euclidean Algorithm
Interestingly, the Euclidan Algorithm works in Z[x], albeit with large numbers intermediately.
This suggests to replace the modular approach to Z[x] by the conceptionally much sipler Euclid,
since arbitrary-precision arithmetic is available.
Walther Neuper <neuper@ist.tugraz.at> [Wed, 17 Jul 2013 07:32:53 +0200] rev 52062
--- heap image for Isac on Isabelle2013 builds
This required introduction of 'session'.
NOTE: building the session raised errors NOT detected
by Build_Isac.thy, cf. 4ecea2fcdc2c