| Fri, 23 Mar 2018 10:14:39 +0100 |
Celem: Test_Isac partially
|
file | diff | annotate |
| Thu, 15 Mar 2018 12:45:31 +0100 |
tuned
|
file | diff | annotate |
| Thu, 15 Mar 2018 10:17:44 +0100 |
separate structure Celem: CALC_ELEMENT, all but Knowledge/
|
file | diff | annotate |
| Wed, 07 Feb 2018 10:24:16 +0100 |
Isabelle2015->17: session identifiers enforced now
|
file | diff | annotate |
| Wed, 13 Jan 2016 14:37:27 +0100 |
cleanup theory imports, part 1
|
file | diff | annotate |
| Mon, 04 Aug 2014 17:03:55 +0200 |
CLEANUP since 347cf013dee3 and restored Test_Isac
|
file | diff | annotate |
| Mon, 23 Jun 2014 09:26:22 +0200 |
ad thehier: read only from finally completed knowledge
|
file | diff | annotate |
| Thu, 19 Jun 2014 07:40:46 +0200 |
ad 967c8a1eb6b1 (2,6) thehier: final repair of KEStore_Elems.add_thes
|
file | diff | annotate |
| Sun, 15 Jun 2014 18:39:59 +0200 |
merged
|
file | diff | annotate |
| Sun, 15 Jun 2014 18:27:23 +0200 |
ad 967c8a1eb6b1 (2,3) thehier: ugly chunk makes Test_Isac run
|
file | diff | annotate |
| Thu, 12 Jun 2014 21:59:15 +0200 |
calls to ML_Context.the_generic_context removed from KEStore.thy because they did not work when called from within a future. However, there are still five instances in other locations yet to be removed.
|
file | diff | annotate |
| Fri, 06 Jun 2014 14:49:18 +0200 |
ad 967c8a1eb6b1 (2): add missing setup KEStore_Elems.add_thes fails
|
file | diff | annotate |
| Thu, 05 Jun 2014 16:41:42 +0200 |
ad 967c8a1eb6b1 (7): remove all code concerned with "thehier = Unsynchronized.ref"
|
file | diff | annotate |
| Thu, 05 Jun 2014 09:20:48 +0200 |
ad 967c8a1eb6b1 (6): switch from "thehier = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Thu, 05 Jun 2014 09:09:53 +0200 |
ad 967c8a1eb6b1 (2): added parallel calls to thehier via Theory_Data
|
file | diff | annotate |
| Thu, 05 Jun 2014 08:53:31 +0200 |
ad 967c8a1eb6b1 (2): complete functions accessing Theory_Data in parallel to ! thehier :=
|
file | diff | annotate |
| Mon, 02 Jun 2014 18:06:27 +0200 |
ad 967c8a1eb6b1 (1): restrict read-access to thehier
|
file | diff | annotate |
| Mon, 02 Jun 2014 17:45:20 +0200 |
ad 967c8a1eb6b1 (0): for thehier start (1)..(7)
|
file | diff | annotate |
| Sat, 31 May 2014 15:53:46 +0200 |
ad 967c8a1eb6b1 (6): switched from 'thehier = Unsynchronized.ref' to Theory_Data
|
file | diff | annotate |
| Tue, 18 Mar 2014 06:36:57 +0100 |
ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to thehier
|
file | diff | annotate |
| Mon, 17 Mar 2014 08:54:48 +0100 |
re-establish construction of thehier
|
file | diff | annotate |
| Mon, 10 Feb 2014 10:49:25 +0100 |
Poly: handling of representations II
|
file | diff | annotate |
| Sun, 02 Feb 2014 02:45:11 +0100 |
ad 967c8a1eb6b1 (6): switched from 'mets = Unsynchronized.ref' to Theory_Data
|
file | diff | annotate |
| Sat, 01 Feb 2014 17:55:42 +0100 |
ad 967c8a1eb6b1 (4): check differences between Theory_Data and 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Sat, 01 Feb 2014 16:44:45 +0100 |
ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Fri, 31 Jan 2014 17:50:50 +0100 |
ad 967c8a1eb6b1 (1): restrict access to 'mets = Unsynchronized'
|
file | diff | annotate |
| Mon, 27 Jan 2014 22:26:51 +0100 |
ad 967c8a1eb6b1 (7): removed all code concerned with 'ptyps = Unsynchronized.ref'
|
file | diff | annotate |
| Mon, 27 Jan 2014 21:58:57 +0100 |
ad 967c8a1eb6b1 (6): switched from 'ptyps = Unsynchronized.ref' to Theory_Data
|
file | diff | annotate |
| Mon, 27 Jan 2014 21:51:10 +0100 |
ad 967c8a1eb6b1 (2): fixed future version of 'fun get_ptyps'
|
file | diff | annotate |
| Mon, 27 Jan 2014 21:49:27 +0100 |
cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
|
file | diff | annotate |
| Mon, 27 Jan 2014 11:09:57 +0100 |
ad 967c8a1eb6b1 (2b): add functions accessing Theory_Data in parallel to those accessing "ptyps = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 26 Jan 2014 01:37:36 +0100 |
ad 967c8a1eb6b1 (2b): for 'ptyps' add functions accessing Theory_Data in parallel to old ones for 'Unsynchronized.ref' in 'test' folder.
|
file | diff | annotate |
| Wed, 22 Jan 2014 23:31:59 +0100 |
ad 967c8a1eb6b1: preparations for step 6 (i.e. switch ptyps to Theory_Data)
|
file | diff | annotate |
| Wed, 22 Jan 2014 20:23:31 +0100 |
ad 967c8a1eb6b1 (3): check differences between Theory_Data and 'Unsynchronized.ref ptyps'
|
file | diff | annotate |
| Tue, 21 Jan 2014 00:27:44 +0100 |
ad 967c8a1eb6b1 (2): for 'ptyps' add functions accessing Theory_Data in parallel to the old ones for 'Unsynchronized.ref'.
|
file | diff | annotate |
| Mon, 20 Jan 2014 16:15:34 +0100 |
ad 967c8a1eb6b1 (1b): restrict access...
|
file | diff | annotate |
| Tue, 19 Nov 2013 22:18:14 +0000 |
switched from "castab = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Tue, 19 Nov 2013 21:37:18 +0000 |
check differences between Theory_Data and "castab = Unsynchronized.ref"
|
file | diff | annotate |
| Tue, 19 Nov 2013 20:08:37 +0000 |
add functions accessing Theory_Data in parallel to those accessing "castab = Unsynchronized.ref"
|
file | diff | annotate |
| Tue, 19 Nov 2013 16:42:06 +0100 |
begin (2) for castab: add functions accessing "Theory_Data"
|
file | diff | annotate |
| Fri, 25 Oct 2013 23:23:41 +0100 |
string_of_calc renamed to check_kestore_calc
|
file | diff | annotate |
| Fri, 25 Oct 2013 20:58:28 +0100 |
removed all code concerned with "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Thu, 24 Oct 2013 15:00:44 +0200 |
removed all code concerned with "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Thu, 24 Oct 2013 14:08:32 +0200 |
notes on "type cal" and "type calc".
|
file | diff | annotate |
| Thu, 24 Oct 2013 00:02:29 +0100 |
switched from "calclist' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Mon, 21 Oct 2013 15:57:27 +0100 |
check differences between Theory_Data and "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Wed, 16 Oct 2013 23:59:43 +0100 |
add functions accessing Theory_Data in parallel to those accessing "calclist' = Unsynchronized.ref
|
file | diff | annotate |
| Mon, 30 Sep 2013 16:22:07 +0200 |
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
|
file | diff | annotate |
| Mon, 30 Sep 2013 11:50:13 +0200 |
last difference between Theory_Data and "ruleset' = Unsynchronized.ref" removed
|
file | diff | annotate |
| Sun, 29 Sep 2013 18:27:37 +0200 |
collected updates since changeset 9690a8d5f1c
|
file | diff | annotate |
| Sun, 22 Sep 2013 18:41:15 +0200 |
check differences between Theory_Data and "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 22 Sep 2013 18:17:25 +0200 |
narrow behaviour of Theory_Data and "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 22 Sep 2013 18:09:05 +0200 |
add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Sun, 22 Sep 2013 17:28:55 +0200 |
shift existing access functions for Unsynchronized.ref to bottom of KEStore.thy
|
file | diff | annotate |
| Fri, 20 Sep 2013 15:30:09 +0200 |
tuned
|
file | diff | annotate |