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
|
Tue, 21 Jan 2014 00:27:44 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (2): for 'ptyps' add functions accessing Theory_Data in parallel to the old ones for 'Unsynchronized.ref'.
|
changeset |
files
|
Mon, 20 Jan 2014 16:15:34 +0100 |
Mathias Lehnfeld |
ad 967c8a1eb6b1 (1b): restrict access...
|
changeset |
files
|
Fri, 17 Jan 2014 14:52:11 +0100 |
Walther Neuper |
Poly: we need an abstract polynomial first, which
|
changeset |
files
|
Wed, 15 Jan 2014 12:59:19 +0100 |
Walther Neuper |
Poly: n-polynomials -- proof of concept less warty
|
changeset |
files
|
Tue, 14 Jan 2014 18:46:56 +0100 |
Walther Neuper |
ad 967c8a1eb6b1 (1a): for 'ptyps' shift types ...
|
changeset |
files
|
Tue, 14 Jan 2014 13:03:25 +0100 |
Walther Neuper |
CLEANUP
|
changeset |
files
|
Fri, 10 Jan 2014 16:24:48 +0100 |
Walther Neuper |
Poly: n-polynomials -- proof of concept less warty
|
changeset |
files
|
Fri, 10 Jan 2014 16:07:24 +0100 |
Walther Neuper |
Poly: added boilerplate by Andreas Lochbihler
|
changeset |
files
|
Mon, 06 Jan 2014 14:10:42 +0100 |
Walther Neuper |
Poly: presently preferred solution for multiple representations
|
changeset |
files
|
Mon, 30 Dec 2013 15:25:12 +0100 |
Walther Neuper |
Poly: yet another trial
|
changeset |
files
|
Fri, 27 Dec 2013 18:18:04 +0100 |
Walther Neuper |
Poly: renamed "npoly" according to other representations
|
changeset |
files
|
Fri, 27 Dec 2013 17:53:56 +0100 |
Walther Neuper |
Poly: svn r79 | haftmann | 2013-12-23 naive representation of n-polynomials -- proof of concept
|
changeset |
files
|
Fri, 27 Dec 2013 17:16:44 +0100 |
Walther Neuper |
Poly: another trial with Andreas Lochbihler's hints
|
changeset |
files
|
Mon, 23 Dec 2013 16:35:24 +0100 |
Walther Neuper |
Poly: first trials with Andreas Lochbihler's hints
|
changeset |
files
|
Mon, 23 Dec 2013 15:19:06 +0100 |
Walther Neuper |
Poly: added Florian's proofs to Wolfgang's version
|
changeset |
files
|
Mon, 23 Dec 2013 14:58:20 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
Mon, 23 Dec 2013 14:57:54 +0100 |
Walther Neuper |
Poly: insert development of polynomial representations
|
changeset |
files
|
Tue, 17 Dec 2013 00:40:49 +0000 |
Mathias Lehnfeld |
tuned
|
changeset |
files
|
Tue, 17 Dec 2013 00:31:59 +0000 |
Mathias Lehnfeld |
(1) started limiting access to "ptyps = Unsynchronized.ref"
|
changeset |
files
|
Thu, 12 Dec 2013 15:16:09 +0100 |
Walther Neuper |
Isabelle2013-1 --> 2013-2: Test_Isac is perfect again
|
changeset |
files
|
Thu, 12 Dec 2013 14:37:15 +0100 |
Walther Neuper |
Isabelle2013-1 --> 2013-2: merged TUG/isa into TUM/isabelle
|
changeset |
files
|
Thu, 12 Dec 2013 14:27:37 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
Thu, 12 Dec 2013 14:26:56 +0100 |
Walther Neuper |
Isabelle2013-1 --> 2013-2: isac's hgignore copied into new Isabelle files
|
changeset |
files
|
Wed, 04 Dec 2013 18:59:20 +0100 |
wenzelm |
remove junk;
|
changeset |
files
|
Wed, 04 Dec 2013 18:38:26 +0100 |
wenzelm |
recover main entry point from d9c88171b393 -- occasionally useful with plain "java -jar jedit.jar";
|
changeset |
files
|
Mon, 02 Dec 2013 15:49:02 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 01 Dec 2013 17:09:35 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 01 Dec 2013 16:35:38 +0100 |
wenzelm |
Added tag Isabelle2013-2-RC3 for changeset aeb21314d078
|
changeset |
files
|