1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Fri Nov 27 20:54:01 2020 +0100
1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sat Nov 28 17:47:43 2020 +0100
1.3 @@ -118,11 +118,12 @@
1.4
1.5 subsection \<open>test runs with Example\<close>
1.6 text \<open>
1.7 - Do in Test_Some.thy:
1.8 + Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
1.9 + So, do ~~$ ./zcoding-to-test.sh and use Test_Some.thy to evaluate
1.10
1.11 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
1.12
1.13 - Starting the Calculation for the Example requires session Isac with Isac.Biegelinie etc.
1.14 + This now gives no error, but also no <Output>. See child of 3ea616c84845.
1.15 \<close>
1.16
1.17 section \<open>Adapt Sledgehammer to write Problem ("Biegelinie", ["Biegelinien"]) to thy\<close>
2.1 --- a/test/Tools/isac/Test_Some.thy Fri Nov 27 20:54:01 2020 +0100
2.2 +++ b/test/Tools/isac/Test_Some.thy Sat Nov 28 17:47:43 2020 +0100
2.3 @@ -95,14 +95,11 @@
2.4
2.5 section \<open>===================================================================================\<close>
2.6 ML \<open>
2.7 -\<close> ML \<open>
2.8 @{theory Calculation}
2.9 \<close> ML \<open>
2.10 @{theory Biegelinie}
2.11 \<close> ML \<open>
2.12 -\<close> ML \<open>
2.13 \<close>
2.14 -
2.15 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>(*.str*)
2.16
2.17