Walther Neuper <walther.neuper@jku.at> [Mon, 22 Mar 2021 16:20:56 +0100] rev 60179
remove notes from Calculation.thy
Walther Neuper <walther.neuper@jku.at> [Mon, 22 Mar 2021 08:31:30 +0100] rev 60178
remove outdated comments and trials
Walther Neuper <walther.neuper@jku.at> [Thu, 18 Mar 2021 13:56:45 +0100] rev 60177
Example takes a single file
Walther Neuper <walther.neuper@jku.at> [Mon, 15 Mar 2021 10:49:53 +0100] rev 60176
resume step 6.10: unsuccessful trials with combination of types on Outer_Syntax
note: test in Calculation.thy has Given: "Traegerlaenge " "Streckenlast " outcommented
Walther Neuper <walther.neuper@jku.at> [Mon, 15 Mar 2021 10:45:12 +0100] rev 60175
/----- finish update Isabelle2020 --> Isabelle2021 for Test_Isac_Short.thy
Walther Neuper <walther.neuper@jku.at> [Mon, 15 Mar 2021 10:04:17 +0100] rev 60174
Isabelle2020->21: th_load with constant string
note: this way bypass InteliJ Idea
Walther Neuper <walther.neuper@jku.at> [Fri, 12 Mar 2021 15:22:39 +0100] rev 60173
Isabelle2020->21: declare "thy_load (isac_example)" to Scala, partially
would involve IntelliJ IDEA;
see https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-March/msg00047.html
Walther Neuper <walther.neuper@jku.at> [Fri, 12 Mar 2021 13:25:51 +0100] rev 60172
Isabelle2020->21: adapt SPARK to tests
Walther Neuper <walther.neuper@jku.at> [Fri, 12 Mar 2021 12:48:55 +0100] rev 60171
Isabelle2020->21: adapt SPARK to ParseC
Walther Neuper <walther.neuper@jku.at> [Mon, 08 Mar 2021 10:04:37 +0100] rev 60170
Isabelle2020->21: Pure and HOL build with updated thm.ML