Walther Neuper <neuper@ist.tugraz.at> [Sat, 01 Feb 2014 00:13:32 +0100] rev 55371
tuned
Walther Neuper <neuper@ist.tugraz.at> [Sat, 01 Feb 2014 00:12:10 +0100] rev 55370
add Notes.thy as collected comments to the code
so text from Collect.thy is shifted to Notes.thy
Walther Neuper <neuper@ist.tugraz.at> [Sat, 01 Feb 2014 00:08:33 +0100] rev 55369
prepare for Notes.thy according to mail discussions
# rename 'a poly to 'a mpoly
# add dummy definitions
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Jan 2014 11:09:45 +0100] rev 55368
tuned
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Jan 2014 10:49:50 +0100] rev 55367
Poly: ----- new setup for abstract poly + representations -----
src/HOL/Library/Poly/Abstract.thy the abstract polynomial
src/HOL/Library/Poly/Collect.thy links abstract and representations
src/HOL/Library/Poly/Rep_Distr_Dense.thy distributive representation
src/HOL/Library/Poly/Rep_Recur_Dense.thy recursive representations
See SOURCE in the initial comment of each file
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Jan 2014 08:21:45 +0100] rev 55366
adapted test setup for test
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Jan 2014 07:37:27 +0100] rev 55365
tuned e8d9d194a96f
Walther Neuper <neuper@ist.tugraz.at> [Tue, 28 Jan 2014 07:04:48 +0100] rev 55364
adapted test setup for tests restored in e8d9d194a96f
test with extend the KEStore require a specific setup:
# "setup {* ... *}" in file "~~/test/../filename.thy"
(NOT Isabelle coding standard)
# the respective SML code is in "~~/test/../filename.sml"
(in order to keept the "imports" phase of Test_Isac.thy short)
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Mon, 27 Jan 2014 22:26:51 +0100] rev 55363
ad 967c8a1eb6b1 (7): removed all code concerned with 'ptyps = Unsynchronized.ref'
Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at> [Mon, 27 Jan 2014 21:58:57 +0100] rev 55362
ad 967c8a1eb6b1 (6): switched from 'ptyps = Unsynchronized.ref' to Theory_Data