| Sat, 08 Mar 2014 10:33:55 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
| Sat, 08 Mar 2014 10:33:34 +0100 |
Walther Neuper |
make specific tests run with Test_Some.thy
|
changeset |
files
|
| Fri, 07 Mar 2014 16:30:24 +0100 |
Walther Neuper |
make specific tests run with Test_Some.thy
|
changeset |
files
|
| Tue, 04 Mar 2014 19:12:52 +0100 |
Walther Neuper |
note on f10dfa200452
|
changeset |
files
|
| Tue, 04 Mar 2014 18:30:20 +0100 |
Walther Neuper |
replaced datatype by typedef 'a mpoly
|
changeset |
files
|
| Sun, 16 Feb 2014 11:44:09 +0100 |
Walther Neuper |
Poly: questions reviewed
|
changeset |
files
|
| Sun, 16 Feb 2014 11:15:41 +0100 |
Walther Neuper |
representation "'a poly_dd" made executable up to scalar multiplication
|
changeset |
files
|
| Fri, 14 Feb 2014 16:30:57 +0100 |
Walther Neuper |
subsections address all features expected for any polynomial
|
changeset |
files
|
| Fri, 14 Feb 2014 16:01:42 +0100 |
Walther Neuper |
representation "'a poly_rd" made executable up to scalar multiplication
|
changeset |
files
|
| Wed, 12 Feb 2014 08:51:17 +0100 |
Walther Neuper |
Variant (e) solved
|
changeset |
files
|
| Tue, 11 Feb 2014 09:02:33 +0100 |
Walther Neuper |
Variant (e): Make abstract algorithms executable
|
changeset |
files
|
| Tue, 11 Feb 2014 07:04:08 +0100 |
Walther Neuper |
cleanup
|
changeset |
files
|
| Mon, 10 Feb 2014 11:14:37 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 10 Feb 2014 11:07:35 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
| Mon, 10 Feb 2014 10:49:25 +0100 |
Walther Neuper |
Poly: handling of representations II
|
changeset |
files
|
| Mon, 10 Feb 2014 08:31:10 +0100 |
Andreas Lochbihler |
clarify possibilities of data refinement in the code generator
|
changeset |
files
|
| Tue, 04 Feb 2014 12:43:13 +0100 |
Walther Neuper |
Poly: handling of representations I
|
changeset |
files
|
| Tue, 04 Feb 2014 12:41:14 +0100 |
Walther Neuper |
handling of representations I
|
changeset |
files
|
| Mon, 03 Feb 2014 16:04:26 +0100 |
Walther Neuper |
checked ad 967c8a1eb6b1 for mets
|
changeset |
files
|
| Sun, 02 Feb 2014 03:09:40 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (7): remove all code concerned with 'mets = Unsynchronized.ref'
|
changeset |
files
|
| Sun, 02 Feb 2014 02:45:11 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (6): switched from 'mets = Unsynchronized.ref' to Theory_Data
|
changeset |
files
|
| Sun, 02 Feb 2014 02:43:04 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2): added missing analog for 'insert_errpats' with 'mets' Theory_Data
|
changeset |
files
|
| Sun, 02 Feb 2014 01:15:13 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2b): in tests, add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
|
changeset |
files
|
| Sat, 01 Feb 2014 17:55:42 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (4): check differences between Theory_Data and 'mets = Unsynchronized.ref'
|
changeset |
files
|
| Sat, 01 Feb 2014 17:14:32 +0100 |
Mathias Lehnfeld |
merged
|
changeset |
files
|
| Sat, 01 Feb 2014 16:58:27 +0100 |
Mathias Lehnfeld |
Isabelle run scripts added to hgignore
|
changeset |
files
|
| Sat, 01 Feb 2014 16:44:45 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
|
changeset |
files
|
| Fri, 31 Jan 2014 17:50:50 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (1): restrict access to 'mets = Unsynchronized'
|
changeset |
files
|
| Sat, 01 Feb 2014 00:13:32 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 01 Feb 2014 00:12:10 +0100 |
Walther Neuper |
add Notes.thy as collected comments to the code
|
changeset |
files
|
| Sat, 01 Feb 2014 00:08:33 +0100 |
Walther Neuper |
prepare for Notes.thy according to mail discussions
|
changeset |
files
|
| Tue, 28 Jan 2014 11:09:45 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Tue, 28 Jan 2014 10:49:50 +0100 |
Walther Neuper |
Poly: ----- new setup for abstract poly + representations -----
|
changeset |
files
|
| Tue, 28 Jan 2014 08:21:45 +0100 |
Walther Neuper |
adapted test setup for test
|
changeset |
files
|
| Tue, 28 Jan 2014 07:37:27 +0100 |
Walther Neuper |
tuned e8d9d194a96f
|
changeset |
files
|
| Tue, 28 Jan 2014 07:04:48 +0100 |
Walther Neuper |
adapted test setup for tests restored in e8d9d194a96f
|
changeset |
files
|
| Mon, 27 Jan 2014 22:26:51 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (7): removed all code concerned with 'ptyps = Unsynchronized.ref'
|
changeset |
files
|
| Mon, 27 Jan 2014 21:58:57 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (6): switched from 'ptyps = Unsynchronized.ref' to Theory_Data
|
changeset |
files
|
| Mon, 27 Jan 2014 21:58:12 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (6): preparation
|
changeset |
files
|
| Mon, 27 Jan 2014 21:51:10 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2): fixed future version of 'fun get_ptyps'
|
changeset |
files
|
| Mon, 27 Jan 2014 21:49:27 +0100 |
Mathias Lehnfeld |
cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
|
changeset |
files
|
| Mon, 27 Jan 2014 13:40:36 +0100 |
Walther Neuper |
test of access
|
changeset |
files
|
| Mon, 27 Jan 2014 11:09:57 +0100 |
Walther Neuper |
ad 967c8a1eb6b1 (2b): add functions accessing Theory_Data in parallel to those accessing "ptyps = Unsynchronized.ref"
|
changeset |
files
|
| Mon, 27 Jan 2014 08:09:29 +0100 |
Walther Neuper |
restored tests on ptyps deleted in f0c78a1e9f85
|
changeset |
files
|
| Sun, 26 Jan 2014 01:37:36 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2b): for 'ptyps' add functions accessing Theory_Data in parallel to old ones for 'Unsynchronized.ref' in 'test' folder.
|
changeset |
files
|
| Sat, 25 Jan 2014 21:06:58 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (1b): access to \!ptyps further restricted
|
changeset |
files
|
| Fri, 24 Jan 2014 18:03:27 +0100 |
Walther Neuper |
deleted valuable tests on ptyps
|
changeset |
files
|
| Fri, 24 Jan 2014 17:55:39 +0100 |
Walther Neuper |
deleted tests concerning "detail"s within a rule set
|
changeset |
files
|
| Fri, 24 Jan 2014 17:34:17 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
| Fri, 24 Jan 2014 17:31:16 +0100 |
Walther Neuper |
confirmed important tests on !ptyps
|
changeset |
files
|
| Fri, 24 Jan 2014 15:44:22 +0100 |
Walther Neuper |
made read access analogous for !ptyps, !mets and !thehier
|
changeset |
files
|
| Fri, 24 Jan 2014 14:54:05 +0100 |
Walther Neuper |
removed an obsolete test file
|
changeset |
files
|
| Wed, 22 Jan 2014 23:31:59 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1: preparations for step 6 (i.e. switch ptyps to Theory_Data)
|
changeset |
files
|
| Wed, 22 Jan 2014 20:23:31 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (3): check differences between Theory_Data and 'Unsynchronized.ref ptyps'
|
changeset |
files
|
| Wed, 22 Jan 2014 18:48:01 +0100 |
Mathias Lehnfeld |
fixed: proof context issues with 'fun term2str' and 'fun pbt2str'
|
changeset |
files
|
| Wed, 22 Jan 2014 15:47:14 +0100 |
Mathias Lehnfeld |
pbt2str functions updated
|
changeset |
files
|
| Wed, 22 Jan 2014 15:31:35 +0100 |
Mathias Lehnfeld |
tuned
|
changeset |
files
|
| Wed, 22 Jan 2014 15:26:14 +0100 |
Mathias Lehnfeld |
"fun strslist2str" added.
|
changeset |
files
|
| Tue, 21 Jan 2014 18:06:35 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
| Tue, 21 Jan 2014 18:06:04 +0100 |
Walther Neuper |
Poly: an abstract type of multivariate polynomials
|
changeset |
files
|