| Wed, 03 Aug 2022 18:17:27 +0200 |
cleanup
|
file | diff | annotate |
| Wed, 03 Aug 2022 13:22:36 +0200 |
replace val example_store = Unsynchronized.ref by Thy_Data
|
file | diff | annotate |
| Thu, 28 Jul 2022 11:43:27 +0200 |
trial on "empty" Example
|
file | diff | annotate |
| Wed, 27 Jul 2022 13:11:43 +0200 |
polish naming
|
file | diff | annotate |
| Tue, 26 Jul 2022 21:29:14 +0200 |
remove ?Problem? from ?Example? avoids redundancy
|
file | diff | annotate |
| Tue, 26 Jul 2022 19:29:09 +0200 |
prepare stepwise input to Example (1)
|
file | diff | annotate |
| Sat, 23 Jul 2022 20:05:25 +0200 |
//continued: investigate Outer_Syntax.command \<^command_keyword>?problem?
|
file | diff | annotate |
| Wed, 20 Jul 2022 11:56:45 +0200 |
question about Outer_Syntax.command \<^command_keyword>?Example?
|
file | diff | annotate |
| Wed, 22 Jun 2022 17:33:45 +0200 |
initialise VSCode_Example with complete Specification
|
file | diff | annotate |
| Mon, 20 Jun 2022 18:37:54 +0200 |
rename functions in o-model.sml
|
file | diff | annotate |
| Mon, 20 Jun 2022 11:51:12 +0200 |
initialise state from intermed. example_store
|
file | diff | annotate |
| Sat, 18 Jun 2022 12:34:29 +0200 |
adapth thy to Demo_Example
|
file | diff | annotate |
| Fri, 17 Jun 2022 12:15:09 +0200 |
start checking input by ISAC
|
file | diff | annotate |
| Thu, 02 Jun 2022 17:53:41 +0200 |
tuned
|
file | diff | annotate |
| Thu, 02 Jun 2022 17:13:44 +0200 |
Calculation 8: add References; bypass "Outer syntax error: keyword Theory_Ref expected"
|
file | diff | annotate |
| Thu, 02 Jun 2022 12:12:42 +0200 |
Calculation 7': model with data from Demo_Example
|
file | diff | annotate |
| Thu, 02 Jun 2022 11:23:52 +0200 |
Calculation 7: shift model input to right place in Demo_Example
|
file | diff | annotate |
| Thu, 02 Jun 2022 09:45:11 +0200 |
Calculation 6''': add argument to Problem
|
file | diff | annotate |
| Wed, 01 Jun 2022 14:37:55 +0200 |
Calculation 6'': add inital keywords
|
file | diff | annotate |
| Wed, 01 Jun 2022 14:30:53 +0200 |
Calculation 6': push "Problem" into Demo_Example
|
file | diff | annotate |
| Wed, 01 Jun 2022 13:36:28 +0200 |
Calculation 5'': cleanup
|
file | diff | annotate |
| Wed, 01 Jun 2022 12:27:05 +0200 |
Calculation 5': cleanup
|
file | diff | annotate |
| Wed, 01 Jun 2022 10:58:36 +0200 |
Calculation 5: narrow headline of "problem" towards "Example"
|
file | diff | annotate |
| Tue, 31 May 2022 19:24:28 +0200 |
Calculation 3': Demo_Example stores values to Theory_Data
|
file | diff | annotate |
| Tue, 31 May 2022 17:33:02 +0200 |
Calculation 3: Demo_Example stored in Theory_Data
|
file | diff | annotate |
| Tue, 31 May 2022 16:21:22 +0200 |
cleanup
|
file | diff | annotate |
| Tue, 31 May 2022 10:17:11 +0200 |
cleanup
|
file | diff | annotate |
| Tue, 31 May 2022 09:57:15 +0200 |
Calculation 2: Demo_Example without ML code
|
file | diff | annotate |
| Tue, 31 May 2022 09:36:02 +0200 |
Calculation 1''': remove test-code from previous changeset 1c8263e775d4
|
file | diff | annotate |
| Tue, 31 May 2022 09:16:12 +0200 |
Calculation 1'': ERROR in Demo_Example.thy, questions in TODO.md
|
file | diff | annotate |
| Sun, 29 May 2022 19:00:35 +0200 |
Calculation 1: minimal changes in code + application
|
file | diff | annotate |
| Sun, 29 May 2022 11:27:34 +0200 |
start Calculation by use of Makarius' "problem" as boilerplate
|
file | diff | annotate |
| Sat, 17 Apr 2021 20:41:09 +0200 |
avoid changes to Isabelle sources:
|
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 |
| Wed, 07 Apr 2021 21:33:01 +0200 |
pwd test by WN
|
file | diff | annotate |
| Mon, 22 Mar 2021 17:22:08 +0100 |
tuned
|
file | diff | annotate |
| Mon, 22 Mar 2021 16:20:56 +0100 |
remove notes from Calculation.thy
|
file | diff | annotate |
| Mon, 22 Mar 2021 08:31:30 +0100 |
remove outdated comments and trials
|
file | diff | annotate |
| Thu, 18 Mar 2021 13:56:45 +0100 |
Example takes a single file
|
file | diff | annotate |
| Mon, 15 Mar 2021 10:04:17 +0100 |
Isabelle2020->21: th_load with constant string
|
file | diff | annotate |
| Fri, 12 Mar 2021 15:22:39 +0100 |
Isabelle2020->21: declare "thy_load (isac_example)" to Scala, partially
|
file | diff | annotate |
| Fri, 12 Mar 2021 12:48:55 +0100 |
Isabelle2020->21: adapt SPARK to ParseC
|
file | diff | annotate |
| Mon, 08 Mar 2021 08:17:28 +0100 |
step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax
|
file | diff | annotate |
| Mon, 01 Mar 2021 16:03:06 +0100 |
step 6.9: errors on Given, RTheory due to "Model" "References" :: diag
|
file | diff | annotate |
| Mon, 01 Mar 2021 12:46:40 +0100 |
step 6.8: "Specification" "Model" :: diag ..both work,
|
file | diff | annotate |
| Sat, 27 Feb 2021 16:59:41 +0100 |
step 6.7: new error on Specification:
|
file | diff | annotate |
| Sat, 27 Feb 2021 16:35:33 +0100 |
step 6.7: describe error on Specification:
|
file | diff | annotate |
| Fri, 26 Feb 2021 19:20:50 +0100 |
step 6.6: prelim. Outer_Syntax..Specification, Model, Given, ..
|
file | diff | annotate |
| Fri, 26 Feb 2021 13:13:03 +0100 |
step 6.5: investigate collision Problem .. Specification; Position?
|
file | diff | annotate |
| Wed, 17 Feb 2021 15:43:34 +0100 |
step 6.4 ~ step 3.5: make Problem independent from SPARK
|
file | diff | annotate |
| 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 |