| Mon, 28 Jul 2014 17:06:16 +0200 |
ad (a): thehier does not contain sym_thmID theorems anymore
|
file | diff | annotate |
| Mon, 23 Jun 2014 09:26:22 +0200 |
ad thehier: read only from finally completed knowledge
|
file | diff | annotate |
| Sun, 22 Jun 2014 15:22:30 +0200 |
CLEANUP since cf8879216db3
|
file | diff | annotate |
| Sun, 22 Jun 2014 14:32:51 +0200 |
ad thehier: add funs grouping thys handled in Isac
|
file | diff | annotate |
| Sun, 22 Jun 2014 14:18:02 +0200 |
ad thehier: link KEStore_Elems to completed IsacKnowledge
|
file | diff | annotate |
| Thu, 19 Jun 2014 08:15:50 +0200 |
ad 967c8a1eb6b1 thehier: cleanup
|
file | diff | annotate |
| Thu, 19 Jun 2014 08:12:08 +0200 |
ad 967c8a1eb6b1 (7) thehier: remove setup keeping tests run since 130602, 227924cdba6a
|
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 18:10:46 +0200 |
plans for approaching Isabelle with Isac
|
file | diff | annotate |
| Thu, 05 Jun 2014 17:56:53 +0200 |
finished transition Isabelle2011-->2013
|
file | diff | annotate |
| Thu, 05 Jun 2014 16:44:36 +0200 |
updated plans for Isabelle2011 --> Isabelle2013
|
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:09:53 +0200 |
ad 967c8a1eb6b1 (2): added parallel calls to thehier via Theory_Data
|
file | diff | annotate |
| Wed, 04 Jun 2014 17:20:40 +0200 |
ad 967c8a1eb6b1 (1): restrict write-access to thehier
|
file | diff | annotate |
| Mon, 02 Jun 2014 18:06:27 +0200 |
ad 967c8a1eb6b1 (1): restrict read-access to thehier
|
file | diff | annotate |
| Tue, 18 Mar 2014 08:56:41 +0100 |
notes on how "Generate representations for ISAC Knowledge"
|
file | diff | annotate |
| Mon, 17 Mar 2014 15:20:15 +0100 |
re-establish tests for thehier
|
file | diff | annotate |
| Mon, 17 Mar 2014 13:56:34 +0100 |
tuned
|
file | diff | annotate |
| Mon, 17 Mar 2014 13:53:19 +0100 |
tuned
|
file | diff | annotate |
| Mon, 17 Mar 2014 08:54:48 +0100 |
re-establish construction of thehier
|
file | diff | annotate |
| Sat, 08 Mar 2014 10:59:41 +0100 |
plans for re-engineering Isac's theory hierarchy
|
file | diff | annotate |
| Sun, 02 Feb 2014 03:09:40 +0100 |
ad 967c8a1eb6b1 (7): remove all code concerned with 'mets = Unsynchronized.ref'
|
file | diff | annotate |
| Sun, 02 Feb 2014 02:43:04 +0100 |
ad 967c8a1eb6b1 (2): added missing analog for 'insert_errpats' with 'mets' 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, 25 Jan 2014 21:06:58 +0100 |
ad 967c8a1eb6b1 (1b): access to \!ptyps further restricted
|
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, 19 Nov 2013 22:23:30 +0000 |
removed all code concerned with "castab = Unsynchronized.ref"
|
file | diff | annotate |
| Tue, 19 Nov 2013 21:37:18 +0000 |
check differences between Theory_Data and "castab = Unsynchronized.ref"
|
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 |
| Mon, 21 Oct 2013 15:57:27 +0100 |
check differences between Theory_Data and "calclist' = Unsynchronized.ref"
|
file | diff | annotate |
| Mon, 21 Oct 2013 09:03:50 +0200 |
"axiomatization" replaces "axioms" preparing for Isabelle2013-1
|
file | diff | annotate |
| Mon, 30 Sep 2013 16:22:07 +0200 |
switched from "ruleset' = Unsynchronized.ref" to Theory_Data
|
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:09:05 +0200 |
add functions accessing Theory_Data in parallel to those accessing "ruleset' = Unsynchronized.ref"
|
file | diff | annotate |
| Mon, 22 Jul 2013 13:52:18 +0200 |
--- Test_Isac.thy runs all tests
|
file | diff | annotate |
| Wed, 17 Jul 2013 07:32:53 +0200 |
--- heap image for Isac on Isabelle2013 builds
|
file | diff | annotate |
| Thu, 11 Jul 2013 16:59:05 +0200 |
tuned
|
file | diff | annotate |
| Thu, 11 Jul 2013 16:58:31 +0200 |
end of improving tests for isac on Isabelle2012
|
file | diff | annotate |
| Fri, 21 Jun 2013 17:53:46 +0200 |
tuned
|
file | diff | annotate |
| Fri, 21 Jun 2013 17:49:24 +0200 |
Test_Isac.thy without errors on Isabelle2012, rewtools.sml:
|
file | diff | annotate |
| Fri, 21 Jun 2013 11:19:18 +0200 |
Test_Isac.thy without errors on Isabelle2012, intermediate
|
file | diff | annotate |
| Fri, 21 Jun 2013 08:06:50 +0200 |
tuned
|
file | diff | annotate |
| Fri, 21 Jun 2013 08:06:16 +0200 |
plans for isac's transitions Isabelle2011-->12 in more detail; errors in tests
|
file | diff | annotate |
| Thu, 20 Jun 2013 17:53:47 +0200 |
manually completed "thehier" such that insert_errpats, insert_fillpats
|
file | diff | annotate |
| Thu, 20 Jun 2013 11:26:56 +0200 |
plans for isac's transitions Isabelle2011-->12 and Isabelle2012-->13
|
file | diff | annotate |
| Sun, 16 Jun 2013 12:31:41 +0200 |
Isabelle2011 --> 2012 intermediate
|
file | diff | annotate |
| Sun, 14 Oct 2012 21:26:02 +0200 |
2011-->2012: "isabelle usedir -b HOL Isac" works
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
| Thu, 20 Sep 2012 10:07:02 +0200 |
added error-pattern "addition-of-fractions"
|
file | diff | annotate |
| Mon, 06 Aug 2012 10:38:11 +0200 |
PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
|
file | diff | annotate |
| Sat, 04 Aug 2012 10:43:07 +0200 |
intermed: isolate tests from others
|
file | diff | annotate |
| Fri, 03 Aug 2012 15:44:39 +0200 |
Build_Thydata.thy with insert_errpats ok
|
file | diff | annotate |
| Thu, 02 Aug 2012 18:39:06 +0200 |
completed interface to dialog-autoring
|
file | diff | annotate |
| Thu, 02 Aug 2012 15:48:57 +0200 |
improved fun insert_fillpats
|
file | diff | annotate |