| Wed, 21 Apr 2021 10:04:17 +0200 |
done TODO caused by ac7426ab0491
|
file | diff | annotate |
| Tue, 20 Apr 2021 16:58:44 +0200 |
replace power ^^^ by \<up>
|
file | diff | annotate |
| Mon, 19 Apr 2021 20:44:18 +0200 |
less ambitious ML_print_depth: 20 instead of 999;
|
file | diff | annotate |
| Mon, 19 Apr 2021 20:33:04 +0200 |
obsolete;
|
file | diff | annotate |
| Mon, 19 Apr 2021 19:55:31 +0200 |
no \<^isac_test> guard for test material: thus the Prover IDE does not have to switch the option "isac_test";
|
file | diff | annotate |
| Mon, 19 Apr 2021 15:02:00 +0200 |
long identifiers for occurences in test/../termC.sml
|
file | diff | annotate |
| Sun, 18 Apr 2021 23:37:59 +0200 |
conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
|
file | diff | annotate |
| Sun, 18 Apr 2021 18:30:31 +0200 |
proper test sessions, but with remaining failures;
|
file | diff | annotate |
| Fri, 16 Apr 2021 22:29:23 +0200 |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
file | diff | annotate |
| Sun, 04 Apr 2021 12:29:42 +0200 |
separate session Specify
|
file | diff | annotate |
| Sun, 17 Jan 2021 15:25:27 +0100 |
step 5.1: separate code for keyword Example to preliminary file
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
| Wed, 09 Dec 2020 14:22:24 +0100 |
adopt new theory identifier also in comments
|
file | diff | annotate |
| Mon, 07 Dec 2020 17:39:21 +0100 |
step 2 of integration: interrupted
|
file | diff | annotate |
| Mon, 26 Oct 2020 13:52:26 +0100 |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
file | diff | annotate |
| Thu, 22 Oct 2020 15:40:41 +0200 |
complete imports to Test_Isac*
|
file | diff | annotate |
| Wed, 07 Oct 2020 10:02:42 +0200 |
/----- finish update Isabelle2019 --> Isabelle2020 for Test_Isac_Short.thy
|
file | diff | annotate |
| Wed, 23 Sep 2020 14:54:38 +0200 |
final isabisac19 on Isabelle2019
|
file | diff | annotate |
| Sun, 02 Aug 2020 12:32:34 +0200 |
shift code from Test_Parse_Isac to src/
|
file | diff | annotate |
| Fri, 31 Jul 2020 12:21:34 +0200 |
prep.2 recursion Problem .. Solution
|
file | diff | annotate |
| Fri, 17 Jul 2020 11:42:20 +0200 |
cleanup Test_Parse*, start parsers for keyword ISAC
|
file | diff | annotate |
| Thu, 02 Jul 2020 09:57:58 +0200 |
test ISAC keywords
|
file | diff | annotate |
| Mon, 29 Jun 2020 17:27:34 +0200 |
new test me' doesn't overload jEdit buffers
|
file | diff | annotate |
| Wed, 03 Jun 2020 11:25:19 +0200 |
follow 2 ancient updates of Library.ML
|
file | diff | annotate |
| Sat, 30 May 2020 14:10:58 +0200 |
resolve hacks finished
|
file | diff | annotate |
| Fri, 29 May 2020 12:43:41 +0200 |
[errors 4, Test_Isac_Short] resolve hacks, part 4: reapired O_Model.complete_for
|
file | diff | annotate |
| Wed, 20 May 2020 12:52:09 +0200 |
standard format for string lists
|
file | diff | annotate |
| Tue, 19 May 2020 12:33:35 +0200 |
adapt test/../Specify/* to new files in src/../Specify/*
|
file | diff | annotate |
| Fri, 15 May 2020 19:31:04 +0200 |
shift code from Specification to References, separate References_Def
|
file | diff | annotate |
| Thu, 14 May 2020 15:06:18 +0200 |
Test_Isac_Short works with P_Specific
|
file | diff | annotate |
| Thu, 14 May 2020 13:33:47 +0200 |
rename Specification -> References, contiued
|
file | diff | annotate |
| Thu, 14 May 2020 09:30:40 +0200 |
start renaming Specification -> References;
|
file | diff | annotate |
| Wed, 13 May 2020 11:34:05 +0200 |
shift code from struct.Specify to appropriate locations
|
file | diff | annotate |
| Tue, 12 May 2020 07:27:21 +0200 |
remove Specify/mstools.sml
|
file | diff | annotate |
| Tue, 12 May 2020 06:37:04 +0200 |
--- we manually open (min.4) imports in Test_Isac_Short.thy
|
file | diff | annotate |
| Mon, 11 May 2020 20:49:27 +0200 |
prep. remove Specify/mstools.sml
|
file | diff | annotate |
| Mon, 11 May 2020 18:06:24 +0200 |
strange ERROR in imports of Test_Isac_Short.thy
|
file | diff | annotate |
| Mon, 11 May 2020 12:25:52 +0200 |
introduce Pre_Conds.T
|
file | diff | annotate |
| Mon, 11 May 2020 11:07:19 +0200 |
separate struct.Refine, Pre_Conds.
|
file | diff | annotate |
| Sun, 10 May 2020 17:26:36 +0200 |
cleanup generate.sml, model.sml
|
file | diff | annotate |
| Sun, 10 May 2020 13:16:56 +0200 |
investigate I_Model
|
file | diff | annotate |
| Fri, 08 May 2020 18:30:21 +0200 |
cleanup O_Model
|
file | diff | annotate |
| Mon, 04 May 2020 16:25:14 +0200 |
shift code specific for specify-phase to Specify/*
|
file | diff | annotate |
| Mon, 04 May 2020 13:27:45 +0200 |
remove unused code
|
file | diff | annotate |
| Mon, 04 May 2020 12:38:16 +0200 |
end cleanup Interpret/*, preliminary
|
file | diff | annotate |
| Mon, 04 May 2020 09:25:51 +0200 |
separate Solve_Step.add, rearrange code, prep. Specify_Step
|
file | diff | annotate |
| Wed, 29 Apr 2020 12:30:51 +0200 |
prep. separation of check Applicable between specify-phase and solve-phase
|
file | diff | annotate |
| Wed, 29 Apr 2020 09:03:01 +0200 |
comments on relation between files.
|
file | diff | annotate |
| Tue, 28 Apr 2020 17:50:18 +0200 |
separate struct.Thy_Present, rename Thy_Html to Thy_Write
|
file | diff | annotate |
| Tue, 28 Apr 2020 15:31:49 +0200 |
assign code from Rtools to appropriate struct.s
|
file | diff | annotate |
| Mon, 27 Apr 2020 16:37:56 +0200 |
clarify types of Subst
|
file | diff | annotate |
| Mon, 27 Apr 2020 12:36:21 +0200 |
separate struct.Subst, rename idenfitiers
|
file | diff | annotate |
| Fri, 24 Apr 2020 08:51:05 +0200 |
separate struct.Error_Pattern, rename identifiers
|
file | diff | annotate |
| Thu, 23 Apr 2020 09:29:56 +0200 |
separate struct. Derive
|
file | diff | annotate |
| Wed, 22 Apr 2020 11:23:30 +0200 |
rename file according to struct.; start renaming with "Spec"
|
file | diff | annotate |
| Tue, 21 Apr 2020 15:42:50 +0200 |
replace Celem. with new struct.s in BaseDefinitions/
|
file | diff | annotate |
| Tue, 21 Apr 2020 10:13:30 +0200 |
derive Problem from Probl_Def, drop funs and types used by Know_Store
|
file | diff | annotate |
| Mon, 20 Apr 2020 16:47:01 +0200 |
rename remaining struct.s Celem5..Celem8
|
file | diff | annotate |
| Mon, 20 Apr 2020 15:54:19 +0200 |
separate Check_Unique, an exercise in higher order funs
|
file | diff | annotate |
| Sun, 19 Apr 2020 11:07:02 +0200 |
switch "activate for Test_Isac .." back to Build_Isac
|
file | diff | annotate |