1.1 --- a/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 11:00:15 2022 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Demo_Example.thy	Tue May 31 16:21:22 2022 +0200
     1.3 @@ -69,20 +69,12 @@
     1.4  section \<open>Stepwise Development\<close>
     1.5  
     1.6  subsection \<open>Specification Phase\<close>
     1.7 -text \<open> UPDATE:
     1.8 -1. The \<open>Example\<close> below is a minimal adaptation of \<open>problem pbl_bieg : "Biegelinien" ..\<close>
     1.9 -  in Knowledge/Biegelinie.thy.
    1.10 -2. GOON
    1.11 +text \<open> 
    1.12 +  stepwise development to be inspected from
    1.13 +  https://hg.risc.uni-linz.ac.at/wneuper/isa/rev/9d98791b4080
    1.14 +  onwards.
    1.15  \<close>
    1.16  
    1.17 -(*
    1.18 -vvvvvvv why raises \<open>Example\<close> exception Option raised (line 82 of "General/basics.ML")? Although 
    1.19 -        * code (Outer_Syntax.command..Example..) and 
    1.20 -        * application (Example pbl_bieg : "Biegelinien".) are exact copies from Makarius?
    1.21 -        * Although the application below with \<open>problem\<close> works?
    1.22 -        * Although \<open>ExampleSPARK\<close> is disambiguated in Calculation_OLD.thy ?!?
    1.23 -        HOW CAN SUCH AN ERROR BE INVESTIGATED ? debugger ? .. ?         
    1.24 -Example problem*)
    1.25  Example pbl_bieg : "Biegelinien" =
    1.26    Method: "IntegrierenUndKonstanteBestimmen2"
    1.27    Given: "Traegerlaenge l_l" "Streckenlast q_q"