| Wed, 08 Apr 2020 14:24:38 +0200 |
separate struct ThyC
|
file | diff | annotate |
| Mon, 16 Sep 2019 13:47:30 +0200 |
Build_Isac.thy , isabelle build and Test_Isac_Short.thy in x86_64_32 mode
|
file | diff | annotate |
| Thu, 12 Sep 2019 14:42:53 +0200 |
/----- finish update Isabelle2018 --> Isabelle2019 for Test_Isac.thy
|
file | diff | annotate |
| Tue, 10 Sep 2019 17:15:41 +0200 |
Isabelle2018->19: unclarified "Exception- Size raised" in Build_Thydata.thy
|
file | diff | annotate |
| Tue, 10 Sep 2019 16:13:28 +0200 |
Isabelle2018->19: rm libisabelle finished, retain interface.sml
|
file | diff | annotate |
| Tue, 03 Sep 2019 12:40:27 +0200 |
lucin: reorganise theories in ProgLang
|
file | diff | annotate |
| Wed, 28 Aug 2019 11:21:26 +0200 |
reorganised MathEngine/ BridgeLibisabelle/
|
file | diff | annotate |
| Mon, 26 Aug 2019 17:40:27 +0200 |
rename Isac.thy --> Isac_Knowledge.thy
|
file | diff | annotate |
| Fri, 23 Aug 2019 17:23:25 +0200 |
remove Delete.thy
|
file | diff | annotate |
| Thu, 22 Aug 2019 16:48:04 +0200 |
lucin: rename Script --> Program
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Thu, 15 Mar 2018 12:42:04 +0100 |
separate structure Celem: CALC_ELEMENT, finished on src/
|
file | diff | annotate |
| Thu, 08 Mar 2018 07:52:06 +0100 |
TermC: error caused by broken test shows: get_theory "Pure" ...
|
file | diff | annotate |
| Fri, 02 Mar 2018 16:19:02 +0100 |
TermC: clean signature, partially
|
file | diff | annotate |
| Wed, 07 Feb 2018 10:24:16 +0100 |
Isabelle2015->17: session identifiers enforced now
|
file | diff | annotate |
| Sat, 20 Jan 2018 15:46:26 +0100 |
------ eq_thy changes to other module
|
file | diff | annotate |
| Fri, 08 Aug 2014 14:01:19 +0200 |
repair data error in thes2file
|
file | diff | annotate |
| Mon, 04 Aug 2014 17:03:55 +0200 |
CLEANUP since 347cf013dee3 and restored Test_Isac
|
file | diff | annotate |
| Mon, 04 Aug 2014 15:54:57 +0200 |
in thehier replaced Threory.axioms_of by MutabelleExtra.thms_of
|
file | diff | annotate |
| 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 |