Walther Neuper <neuper@ist.tugraz.at> [Sat, 08 Mar 2014 10:33:55 +0100] rev 55399
merged
Walther Neuper <neuper@ist.tugraz.at> [Sat, 08 Mar 2014 10:33:34 +0100] rev 55398
make specific tests run with Test_Some.thy
needs to import Build_Thydata -- like Test_Isac
Walther Neuper <neuper@ist.tugraz.at> [Fri, 07 Mar 2014 16:30:24 +0100] rev 55397
make specific tests run with Test_Some.thy
these tests require Test_KEStore_Elems defined in ADDTESTS/...
Walther Neuper <neuper@ist.tugraz.at> [Tue, 04 Mar 2014 19:12:52 +0100] rev 55396
note on f10dfa200452
this previous changeset contains obsolete Notes.thy
(prepared for discussion in Munich Feb.17/18)
Walther Neuper <neuper@ist.tugraz.at> [Tue, 04 Mar 2014 18:30:20 +0100] rev 55395
replaced datatype by typedef 'a mpoly
what is broken by replacement is marked (***):
5 proofs and value for total_degree
Walther Neuper <neuper@ist.tugraz.at> [Sun, 16 Feb 2014 11:44:09 +0100] rev 55394
Poly: questions reviewed
Walther Neuper <neuper@ist.tugraz.at> [Sun, 16 Feb 2014 11:15:41 +0100] rev 55393
representation "'a poly_dd" made executable up to scalar multiplication
if only updating Rep_Distr_Dense.thy, in Collect.thy an incomprehensible error is raised by:
lift_definition dd_of_some :: "'a :: zero mpoly ? 'a poly_dd"
is "TODO" oops
ERROR: exception TYPE raised (line 420 of "type.ML"):
Type variable has two distinct sorts
?'a
?'a
Walther Neuper <neuper@ist.tugraz.at> [Fri, 14 Feb 2014 16:30:57 +0100] rev 55392
subsections address all features expected for any polynomial
Walther Neuper <neuper@ist.tugraz.at> [Fri, 14 Feb 2014 16:01:42 +0100] rev 55391
representation "'a poly_rd" made executable up to scalar multiplication
quick and dirty without proofs (to be copied from HOL/Library/Polynomial.thy)
Walther Neuper <neuper@ist.tugraz.at> [Wed, 12 Feb 2014 08:51:17 +0100] rev 55390
Variant (e) solved
The solution was evident and is understood now.