Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 08:41:45 +0100] rev 60164
final isabisac20 on Isabelle2020
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
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
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.
Walther Neuper <walther.neuper@jku.at> [Sat, 27 Feb 2021 16:59:41 +0100] rev 60160
step 6.7: new 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.
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
Walther Neuper <walther.neuper@jku.at> [Fri, 26 Feb 2021 13:13:03 +0100] rev 60157
step 6.5: investigate collision Problem .. Specification; Position?
Walther Neuper <walther.neuper@jku.at> [Wed, 17 Feb 2021 15:43:34 +0100] rev 60156
step 6.4 ~ step 3.5: make Problem independent from SPARK
Walther Neuper <walther.neuper@jku.at> [Thu, 11 Feb 2021 17:45:29 +0100] rev 60155
step 6.3: prep. clean Outer_Syntax..Problem from SPARK code