Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Mon, 10 Mar 2014 21:07:35 +0100] rev 55402
user session management now parallel
appendFormula uses futures.
Walther Neuper <neuper@ist.tugraz.at> [Sat, 08 Mar 2014 11:07:52 +0100] rev 55401
Poly: deleted, has got a separate repository
Walther Neuper <neuper@ist.tugraz.at> [Sat, 08 Mar 2014 10:59:41 +0100] rev 55400
plans for re-engineering Isac's theory hierarchy
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