| Tue, 13 Apr 2021 13:20:05 +0200 |
Walther Neuper |
trial with setup for session "Doc", unsuccessful
|
changeset |
files
|
| Thu, 08 Apr 2021 13:27:27 +0200 |
wenzelm |
avoid odd clones of Isabelle latex styles:
|
changeset |
files
|
| Thu, 08 Apr 2021 13:09:44 +0200 |
wenzelm |
proper setup for "Doc" sessions;
|
changeset |
files
|
| Mon, 22 Mar 2021 14:47:06 +0100 |
wenzelm |
do not suppress etc/settings: important for Isabelle component setup;
|
changeset |
files
|
| Wed, 07 Apr 2021 21:33:01 +0200 |
Walther Neuper |
pwd test by WN
|
changeset |
files
|
| Tue, 06 Apr 2021 15:52:27 +0200 |
Walther Neuper |
add text for Specify_Phase
|
changeset |
files
|
| Sun, 04 Apr 2021 13:31:04 +0200 |
Walther Neuper |
new session for Doc/Specify_Phase, incomplete
|
changeset |
files
|
| Sun, 04 Apr 2021 12:29:42 +0200 |
Walther Neuper |
separate session Specify
|
changeset |
files
|
| Sat, 03 Apr 2021 15:27:52 +0200 |
Walther Neuper |
review and update directories in Build_Isac
|
changeset |
files
|
| Mon, 22 Mar 2021 17:22:08 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 22 Mar 2021 16:20:56 +0100 |
Walther Neuper |
remove notes from Calculation.thy
|
changeset |
files
|
| Mon, 22 Mar 2021 08:31:30 +0100 |
Walther Neuper |
remove outdated comments and trials
|
changeset |
files
|
| Thu, 18 Mar 2021 13:56:45 +0100 |
Walther Neuper |
Example takes a single file
|
changeset |
files
|
| Mon, 15 Mar 2021 10:49:53 +0100 |
Walther Neuper |
resume step 6.10: unsuccessful trials with combination of types on Outer_Syntax
|
changeset |
files
|
| Mon, 15 Mar 2021 10:45:12 +0100 |
Walther Neuper |
/----- finish update Isabelle2020 --> Isabelle2021 for Test_Isac_Short.thy
|
changeset |
files
|
| Mon, 15 Mar 2021 10:04:17 +0100 |
Walther Neuper |
Isabelle2020->21: th_load with constant string
|
changeset |
files
|
| Fri, 12 Mar 2021 15:22:39 +0100 |
Walther Neuper |
Isabelle2020->21: declare "thy_load (isac_example)" to Scala, partially
|
changeset |
files
|
| Fri, 12 Mar 2021 13:25:51 +0100 |
Walther Neuper |
Isabelle2020->21: adapt SPARK to tests
|
changeset |
files
|
| Fri, 12 Mar 2021 12:48:55 +0100 |
Walther Neuper |
Isabelle2020->21: adapt SPARK to ParseC
|
changeset |
files
|
| Mon, 08 Mar 2021 10:04:37 +0100 |
Walther Neuper |
Isabelle2020->21: Pure and HOL build with updated thm.ML
|
changeset |
files
|
| Mon, 08 Mar 2021 09:43:59 +0100 |
Walther Neuper |
Isabelle2020->21: separate appearance of Isac from Isabelle
|
changeset |
files
|
| Mon, 08 Mar 2021 09:40:09 +0100 |
Walther Neuper |
Isabelle2020->21: notify Isabelle about Isac sessions
|
changeset |
files
|
| Mon, 08 Mar 2021 09:35:14 +0100 |
Walther Neuper |
Isabelle2020->21: define storage for installation-specific settings
|
changeset |
files
|
| Mon, 08 Mar 2021 09:11:09 +0100 |
Walther Neuper |
\----- start update Isabelle2020 --> Isabelle2021
|
changeset |
files
|
| Mon, 08 Mar 2021 08:42:05 +0100 |
Walther Neuper |
Added tag isabisac20 for changeset 573da5c3a9f6
|
changeset |
files
|
| Mon, 08 Mar 2021 08:41:45 +0100 |
Walther Neuper |
final isabisac20 on Isabelle2020
isabisac20
|
changeset |
files
|
| Mon, 08 Mar 2021 08:17:28 +0100 |
Walther Neuper |
step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax
|
changeset |
files
|
| Mon, 01 Mar 2021 16:03:06 +0100 |
Walther Neuper |
step 6.9: errors on Given, RTheory due to "Model" "References" :: diag
|
changeset |
files
|
| Mon, 01 Mar 2021 12:46:40 +0100 |
Walther Neuper |
step 6.8: "Specification" "Model" :: diag ..both work,
|
changeset |
files
|
| Sat, 27 Feb 2021 16:59:41 +0100 |
Walther Neuper |
step 6.7: new error on Specification:
|
changeset |
files
|
| Sat, 27 Feb 2021 16:35:33 +0100 |
Walther Neuper |
step 6.7: describe error on Specification:
|
changeset |
files
|
| Fri, 26 Feb 2021 19:20:50 +0100 |
Walther Neuper |
step 6.6: prelim. Outer_Syntax..Specification, Model, Given, ..
|
changeset |
files
|
| Fri, 26 Feb 2021 13:13:03 +0100 |
Walther Neuper |
step 6.5: investigate collision Problem .. Specification; Position?
|
changeset |
files
|
| Wed, 17 Feb 2021 15:43:34 +0100 |
Walther Neuper |
step 6.4 ~ step 3.5: make Problem independent from SPARK
|
changeset |
files
|
| Thu, 11 Feb 2021 17:45:29 +0100 |
Walther Neuper |
step 6.3: prep. clean Outer_Syntax..Problem from SPARK code
|
changeset |
files
|
| Wed, 03 Feb 2021 16:39:44 +0100 |
Walther Neuper |
Isac's MethodC not shadowing Isabelle's Method
|
changeset |
files
|
| Wed, 03 Feb 2021 15:21:12 +0100 |
Walther Neuper |
step 6.2: check test-Example: same errors with ParseC.problem .. ParseC.problem_headline
|
changeset |
files
|
| Wed, 03 Feb 2021 14:53:37 +0100 |
Walther Neuper |
step 5.1: adapt ParseC.specification to new keywords
|
changeset |
files
|
| Tue, 26 Jan 2021 12:46:12 +0100 |
Walther Neuper |
step 6> use SPARK as a model for checking input to Model
|
changeset |
files
|
| Fri, 22 Jan 2021 16:03:15 +0100 |
Walther Neuper |
step 5.5: for devel. make test-example independent from session Isac
|
changeset |
files
|
| Fri, 22 Jan 2021 14:56:44 +0100 |
Walther Neuper |
step 5.4: clarify dependencies of BridgeJEdit.thy
|
changeset |
files
|
| Fri, 22 Jan 2021 12:31:19 +0100 |
Walther Neuper |
step 5.3: separate code for keyword Problem to preliminary file
|
changeset |
files
|
| Fri, 22 Jan 2021 11:27:47 +0100 |
Walther Neuper |
step 5.2: shift tests from Test_Parse_Isac.thy to test/../parseC.sml
|
changeset |
files
|
| Sun, 17 Jan 2021 15:25:27 +0100 |
Walther Neuper |
step 5.1: separate code for keyword Example to preliminary file
|
changeset |
files
|
| Sun, 17 Jan 2021 13:16:25 +0100 |
Walther Neuper |
step 5: cleanup previous steps; status quo
|
changeset |
files
|
| Thu, 14 Jan 2021 16:14:27 +0100 |
Walther Neuper |
step 4.8: close all gaps in trace of SPARK gcd
|
changeset |
files
|
| Mon, 11 Jan 2021 13:01:08 +0100 |
Walther Neuper |
try to close 2 gaps in trace
|
changeset |
files
|
| Wed, 06 Jan 2021 11:17:28 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Tue, 05 Jan 2021 17:29:39 +0100 |
Walther Neuper |
step 4.7: cannot fill 2 gaps tracing Outer_Syntax .. Output.report
|
changeset |
files
|
| Mon, 21 Dec 2020 15:13:49 +0100 |
Walther Neuper |
step 4.6: two gaps in trace on SPARK
|
changeset |
files
|
| Mon, 21 Dec 2020 11:55:10 +0100 |
Walther Neuper |
step 4.5: separate trace for specific proof element
|
changeset |
files
|
| Thu, 17 Dec 2020 18:00:27 +0100 |
Walther Neuper |
step 4.4: call hierarchy up from Syntax.check_terms, partially
|
changeset |
files
|
| Thu, 17 Dec 2020 11:45:12 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Thu, 17 Dec 2020 11:42:18 +0100 |
Walther Neuper |
step 4.3: parse Problem + Specification; this is inappropriate..
|
changeset |
files
|
| Thu, 17 Dec 2020 11:22:53 +0100 |
Walther Neuper |
cleanup
|
changeset |
files
|
| Thu, 17 Dec 2020 09:10:30 +0100 |
Walther Neuper |
step 4.2: writeln at calling Output.report uncover some of proof handling
|
changeset |
files
|
| Wed, 16 Dec 2020 16:25:55 +0100 |
Walther Neuper |
step 4.1: @{print} at calling Output.report fails
|
changeset |
files
|
| Tue, 15 Dec 2020 15:10:38 +0100 |
Walther Neuper |
step 4: use Naproche as a model for checking input
|
changeset |
files
|
| Mon, 14 Dec 2020 15:04:10 +0100 |
Walther Neuper |
step 3.4++: previous ROOT.ML raised error during build from theory
|
changeset |
files
|
| Fri, 11 Dec 2020 18:34:10 +0100 |
Walther Neuper |
step 3.4+: where in src/Pure can @{print} be used
|
changeset |
files
|