| Thu, 10 Dec 2020 09:16:44 +0100 |
Walther Neuper |
step 3.3: shallow embedding of ParseC.problem_headline
|
changeset |
files
|
| Wed, 09 Dec 2020 16:24:26 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 09 Dec 2020 14:37:10 +0100 |
Walther Neuper |
step 3.2: prep.data for start of specify-phase
|
changeset |
files
|
| Wed, 09 Dec 2020 14:22:24 +0100 |
Walther Neuper |
adopt new theory identifier also in comments
|
changeset |
files
|
| Tue, 08 Dec 2020 17:10:18 +0100 |
Walther Neuper |
step 3.1: transfer data from Example to Problem
|
changeset |
files
|
| Tue, 08 Dec 2020 13:39:52 +0100 |
Walther Neuper |
step 3: use spark_vc as model for starting work on SpecificationC.T
|
changeset |
files
|
| Mon, 07 Dec 2020 19:57:39 +0100 |
Walther Neuper |
step 1.4: rename new code starting Example according to Isac
|
changeset |
files
|
| Mon, 07 Dec 2020 17:39:21 +0100 |
Walther Neuper |
step 2 of integration: interrupted
|
changeset |
files
|
| Wed, 02 Dec 2020 12:32:30 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 28 Nov 2020 17:58:35 +0100 |
Walther Neuper |
Step 2 of integration: use Sledgehammer as model to make kernel creating proof-templates presented via PIDE
|
changeset |
files
|
| Sat, 28 Nov 2020 17:47:43 +0100 |
Walther Neuper |
Test_Some Example reports no error and no <Output>
|
changeset |
files
|
| Fri, 27 Nov 2020 20:54:01 +0100 |
Walther Neuper |
remove obsolete test code, finished
|
changeset |
files
|
| Fri, 27 Nov 2020 20:25:58 +0100 |
Walther Neuper |
remove obsolete test code
|
changeset |
files
|
| Fri, 27 Nov 2020 18:19:04 +0100 |
Walther Neuper |
Test_Some Example still reports the result from g_c_d
|
changeset |
files
|
| Fri, 27 Nov 2020 16:53:08 +0100 |
Walther Neuper |
integration 3: push new code down to storing by Theory_Data
|
changeset |
files
|
| Thu, 26 Nov 2020 12:24:37 +0100 |
Walther Neuper |
initialise Calculation finished, check SPARK
|
changeset |
files
|
| Wed, 25 Nov 2020 16:10:24 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 25 Nov 2020 12:44:43 +0100 |
Walther Neuper |
adapt initialise Calculation to PIDE
|
changeset |
files
|
| Wed, 25 Nov 2020 09:14:14 +0100 |
Walther Neuper |
integration 2: make Outer\_Syntax..Example handle Isac file..
|
changeset |
files
|
| Tue, 24 Nov 2020 16:17:53 +0100 |
Walther Neuper |
remove @{print} for investigation parsing
|
changeset |
files
|
| Tue, 24 Nov 2020 15:47:14 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Tue, 24 Nov 2020 15:45:08 +0100 |
Walther Neuper |
integration 1: make Outer\_Syntax..Example run as spark_open ?greatest_common_divisor/g_c_d?
|
changeset |
files
|
| Mon, 23 Nov 2020 12:58:52 +0100 |
Walther Neuper |
shift new code into appropriate file
|
changeset |
files
|
| Mon, 23 Nov 2020 11:44:36 +0100 |
Walther Neuper |
Adapt SPARK's code for parsing Formalise.T
|
changeset |
files
|
| Sun, 22 Nov 2020 13:41:51 +0100 |
Walther Neuper |
extend testbed for SPARK to Fdl_Parser.vcs
|
changeset |
files
|
| Thu, 19 Nov 2020 16:58:42 +0100 |
Walther Neuper |
shift section <Adapt SPARK's parser -> parse Formalise.T>
|
changeset |
files
|
| Tue, 17 Nov 2020 14:52:57 +0100 |
Walther Neuper |
testbed for SPARK parsing g_c_d.siv
|
changeset |
files
|
| Mon, 16 Nov 2020 11:41:02 +0100 |
Walther Neuper |
adapt to session Isac now built upon HOL-SPARK
|
changeset |
files
|
| Mon, 16 Nov 2020 10:26:40 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sun, 15 Nov 2020 15:26:52 +0100 |
Walther Neuper |
insert @{print} to analyse HOL-SPARK parsing g_c_d.siv
|
changeset |
files
|
| Wed, 11 Nov 2020 17:27:11 +0100 |
Walther Neuper |
intermediately build Isac on HOL-SPARK
|
changeset |
files
|
| Wed, 04 Nov 2020 09:59:30 +0100 |
Walther Neuper |
separate code for Example from spark_open, resolve name clash
|
changeset |
files
|
| Mon, 02 Nov 2020 15:16:07 +0100 |
Walther Neuper |
prepare Outer_Syntax.command..spark_open as model
|
changeset |
files
|
| Mon, 26 Oct 2020 13:52:26 +0100 |
Walther Neuper |
copy Outer_Syntax.command..spark_open as model for Isac Calculation
|
changeset |
files
|
| Sat, 24 Oct 2020 12:31:22 +0200 |
Walther Neuper |
exercise in manual type inference
|
changeset |
files
|
| Thu, 22 Oct 2020 16:26:45 +0200 |
Walther Neuper |
tuned2
|
changeset |
files
|
| Thu, 22 Oct 2020 16:19:28 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Thu, 22 Oct 2020 16:15:27 +0200 |
Walther Neuper |
start implementing Outer_Syntax.command for Isac calculations
|
changeset |
files
|
| Thu, 22 Oct 2020 15:40:41 +0200 |
Walther Neuper |
complete imports to Test_Isac*
|
changeset |
files
|
| Thu, 22 Oct 2020 14:03:40 +0200 |
Walther Neuper |
various trials to decompose Isabelle's proof machinery
|
changeset |
files
|
| Thu, 08 Oct 2020 10:05:33 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 07 Oct 2020 17:47:18 +0200 |
Walther Neuper |
cp non-recursive problem parser from Test_Parse_Isac to parseC.sml
|
changeset |
files
|
| Wed, 07 Oct 2020 12:15:31 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 07 Oct 2020 11:52:54 +0200 |
Walther Neuper |
resume parsers for shifting Isac inbetween Isabelle/jEdit and Isabelle/HOL
|
changeset |
files
|
| Wed, 07 Oct 2020 10:02:42 +0200 |
Walther Neuper |
/----- finish update Isabelle2019 --> Isabelle2020 for Test_Isac_Short.thy
|
changeset |
files
|
| Wed, 07 Oct 2020 09:57:35 +0200 |
Walther Neuper |
Isabelle2019->20: adapt to new handling of quotes in mixfix, finished
|
changeset |
files
|
| Wed, 07 Oct 2020 09:45:07 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 07 Oct 2020 09:31:10 +0200 |
Walther Neuper |
Isabelle2019->20: adapt to new session requirements continued
|
changeset |
files
|
| Tue, 06 Oct 2020 12:44:42 +0200 |
Walther Neuper |
Isabelle2019->20: session Isac works again
|
changeset |
files
|
| Tue, 06 Oct 2020 12:42:25 +0200 |
Walther Neuper |
Isabelle2019->20: adapt to new handling of quotes in mixfix
|
changeset |
files
|
| Mon, 05 Oct 2020 12:22:51 +0200 |
Walther Neuper |
cleanup CLEANUP
|
changeset |
files
|
| Mon, 05 Oct 2020 12:16:16 +0200 |
Walther Neuper |
Isabelle2019->20: adapt to new session requirements
|
changeset |
files
|
| Mon, 05 Oct 2020 12:05:10 +0200 |
Walther Neuper |
Isabelle2019->20: strange error in Biegelinie, tackled later
|
changeset |
files
|
| Mon, 05 Oct 2020 11:35:42 +0200 |
Walther Neuper |
tests on new session requirements
|
changeset |
files
|
| Sat, 03 Oct 2020 15:58:57 +0200 |
Walther Neuper |
revise .hgignore (NOT working as expected)
|
changeset |
files
|
| Fri, 25 Sep 2020 10:15:33 +0200 |
Walther Neuper |
bypass checking Doc/Lucas_Interpreter
|
changeset |
files
|
| Thu, 24 Sep 2020 15:48:52 +0200 |
Walther Neuper |
adopt new field inf Thm record, finished
|
changeset |
files
|
| Thu, 24 Sep 2020 13:11:51 +0200 |
Walther Neuper |
adopt new field inf Thm record
|
changeset |
files
|
| Thu, 24 Sep 2020 12:58:31 +0200 |
Walther Neuper |
Isabelle2019->20: Pure and HOL build with updated thm.ML
|
changeset |
files
|
| Thu, 24 Sep 2020 12:56:19 +0200 |
Walther Neuper |
Isabelle2019->20: notify Isabelle about Isac sessions
|
changeset |
files
|