Mon, 08 Mar 2021 09:35:14 +0100Isabelle2020->21: define storage for installation-specific settings
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 09:35:14 +0100] rev 60167
Isabelle2020->21: define storage for installation-specific settings

Mon, 08 Mar 2021 09:11:09 +0100\----- start update Isabelle2020 --> Isabelle2021
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 09:11:09 +0100] rev 60166
\----- start update Isabelle2020 --> Isabelle2021

Mon, 08 Mar 2021 08:42:05 +0100Added tag isabisac20 for changeset 573da5c3a9f6
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 08:42:05 +0100] rev 60165
Added tag isabisac20 for changeset 573da5c3a9f6

Mon, 08 Mar 2021 08:41:45 +0100final isabisac20 on Isabelle2020 isabisac20
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 08:41:45 +0100] rev 60164
final isabisac20 on Isabelle2020

Mon, 08 Mar 2021 08:17:28 +0100step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 08:17:28 +0100] rev 60163
step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax

note: test in Calculation.thy is outcommented

Mon, 01 Mar 2021 16:03:06 +0100step 6.9: errors on Given, RTheory due to "Model" "References" :: diag
Walther Neuper <walther.neuper@jku.at> [Mon, 01 Mar 2021 16:03:06 +0100] rev 60162
step 6.9: errors on Given, RTheory due to "Model" "References" :: diag

Mon, 01 Mar 2021 12:46:40 +0100step 6.8: "Specification" "Model" :: diag ..both work,
Walther Neuper <walther.neuper@jku.at> [Mon, 01 Mar 2021 12:46:40 +0100] rev 60161
step 6.8: "Specification" "Model" :: diag ..both work,

but the same error is now at Given: thus provide correct type there.

Sat, 27 Feb 2021 16:59:41 +0100step 6.7: new error on Specification:
Walther Neuper <walther.neuper@jku.at> [Sat, 27 Feb 2021 16:59:41 +0100] rev 60160
step 6.7: new error on Specification:

Sat, 27 Feb 2021 16:35:33 +0100step 6.7: describe error on Specification:
Walther Neuper <walther.neuper@jku.at> [Sat, 27 Feb 2021 16:35:33 +0100] rev 60159
step 6.7: describe error on Specification:

reason for the error seems to be, that no context is transferred.

Fri, 26 Feb 2021 19:20:50 +0100step 6.6: prelim. Outer_Syntax..Specification, Model, Given, ..
Walther Neuper <walther.neuper@jku.at> [Fri, 26 Feb 2021 19:20:50 +0100] rev 60158
step 6.6: prelim. Outer_Syntax..Specification, Model, Given, ..

notes:
* 1 error on "Specification"
* finding: scanner's scopes are delimited by subsequent command keyword