Thu, 11 Feb 2021 17:45:29 +0100 |
step 6.3: prep. clean Outer_Syntax..Problem from SPARK code
|
file | diff | annotate |
Wed, 03 Feb 2021 15:21:12 +0100 |
step 6.2: check test-Example: same errors with ParseC.problem .. ParseC.problem_headline
|
file | diff | annotate |
Tue, 26 Jan 2021 12:46:12 +0100 |
step 6> use SPARK as a model for checking input to Model
|
file | diff | annotate |
Fri, 22 Jan 2021 16:03:15 +0100 |
step 5.5: for devel. make test-example independent from session Isac
|
file | diff | annotate |
Fri, 22 Jan 2021 14:56:44 +0100 |
step 5.4: clarify dependencies of BridgeJEdit.thy
|
file | diff | annotate |
Fri, 22 Jan 2021 12:31:19 +0100 |
step 5.3: separate code for keyword Problem to preliminary file
|
file | diff | annotate |
Fri, 22 Jan 2021 11:27:47 +0100 |
step 5.2: shift tests from Test_Parse_Isac.thy to test/../parseC.sml
|
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 |
Thu, 17 Dec 2020 09:10:30 +0100 |
step 4.2: writeln at calling Output.report uncover some of proof handling
|
file | diff | annotate |
Wed, 16 Dec 2020 16:25:55 +0100 |
step 4.1: @{print} at calling Output.report fails
|
file | diff | annotate |
Tue, 15 Dec 2020 15:10:38 +0100 |
step 4: use Naproche as a model for checking input
|
file | diff | annotate |
Thu, 10 Dec 2020 14:38:32 +0100 |
step 3.4: stop SPARK as a model for investigating Isabelle's proof machinery
|
file | diff | annotate |
Thu, 10 Dec 2020 09:16:44 +0100 |
step 3.3: shallow embedding of ParseC.problem_headline
|
file | diff | annotate |
Wed, 09 Dec 2020 16:24:26 +0100 |
tuned
|
file | diff | annotate |
Wed, 09 Dec 2020 14:37:10 +0100 |
step 3.2: prep.data for start of specify-phase
|
file | diff | annotate |
Tue, 08 Dec 2020 17:10:18 +0100 |
step 3.1: transfer data from Example to Problem
|
file | diff | annotate |
Tue, 08 Dec 2020 13:39:52 +0100 |
step 3: use spark_vc as model for starting work on SpecificationC.T
|
file | diff | annotate |
Mon, 07 Dec 2020 19:57:39 +0100 |
step 1.4: rename new code starting Example according to Isac
|
file | diff | annotate |
Mon, 07 Dec 2020 17:39:21 +0100 |
step 2 of integration: interrupted
|
file | diff | annotate |
Sat, 28 Nov 2020 17:58:35 +0100 |
Step 2 of integration: use Sledgehammer as model to make kernel creating proof-templates presented via PIDE
|
file | diff | annotate |
Sat, 28 Nov 2020 17:47:43 +0100 |
Test_Some Example reports no error and no <Output>
|
file | diff | annotate |
Fri, 27 Nov 2020 20:54:01 +0100 |
remove obsolete test code, finished
|
file | diff | annotate |
Fri, 27 Nov 2020 20:25:58 +0100 |
remove obsolete test code
|
file | diff | annotate |
Fri, 27 Nov 2020 18:19:04 +0100 |
Test_Some Example still reports the result from g_c_d
|
file | diff | annotate |
Fri, 27 Nov 2020 16:53:08 +0100 |
integration 3: push new code down to storing by Theory_Data
|
file | diff | annotate |
Thu, 26 Nov 2020 12:24:37 +0100 |
initialise Calculation finished, check SPARK
|
file | diff | annotate |
Wed, 25 Nov 2020 16:10:24 +0100 |
tuned
|
file | diff | annotate |
Wed, 25 Nov 2020 12:44:43 +0100 |
adapt initialise Calculation to PIDE
|
file | diff | annotate |
Wed, 25 Nov 2020 09:14:14 +0100 |
integration 2: make Outer\_Syntax..Example handle Isac file..
|
file | diff | annotate |
Tue, 24 Nov 2020 16:17:53 +0100 |
remove @{print} for investigation parsing
|
file | diff | annotate |
Tue, 24 Nov 2020 15:47:14 +0100 |
tuned
|
file | diff | annotate |
Tue, 24 Nov 2020 15:45:08 +0100 |
integration 1: make Outer\_Syntax..Example run as spark_open ?greatest_common_divisor/g_c_d?
|
file | diff | annotate |
Mon, 23 Nov 2020 12:58:52 +0100 |
shift new code into appropriate file
|
file | diff | annotate |
Mon, 23 Nov 2020 11:44:36 +0100 |
Adapt SPARK's code for parsing Formalise.T
|
file | diff | annotate |
Sun, 22 Nov 2020 13:41:51 +0100 |
extend testbed for SPARK to Fdl_Parser.vcs
|
file | diff | annotate |
Thu, 19 Nov 2020 16:58:42 +0100 |
shift section <Adapt SPARK's parser -> parse Formalise.T>
|
file | diff | annotate |
Tue, 17 Nov 2020 14:52:57 +0100 |
testbed for SPARK parsing g_c_d.siv
|
file | diff | annotate |
Mon, 16 Nov 2020 11:41:02 +0100 |
adapt to session Isac now built upon HOL-SPARK
|
file | diff | annotate |
Mon, 16 Nov 2020 10:26:40 +0100 |
tuned
|
file | diff | annotate |
Sun, 15 Nov 2020 15:26:52 +0100 |
insert @{print} to analyse HOL-SPARK parsing g_c_d.siv
|
file | diff | annotate |
Wed, 04 Nov 2020 09:59:30 +0100 |
separate code for Example from spark_open, resolve name clash
|
file | diff | annotate |
Mon, 02 Nov 2020 15:16:07 +0100 |
prepare Outer_Syntax.command..spark_open as model
|
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 |