1.1 --- a/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Thu Aug 04 12:48:37 2022 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/VSCode_Example.thy	Thu Aug 04 12:50:19 2022 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  \<close>
     1.5  text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
     1.6  
     1.7 -Example "Diff_App/No.123 a"
     1.8 +Example "Diff_App-No.123a"
     1.9    Specification:
    1.10      Model:
    1.11        Given: \<open>Constants r = 7\<close>
    1.12 @@ -69,7 +69,7 @@
    1.13  \<close>
    1.14  text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
    1.15  
    1.16 -Example "Diff_App/No.123 a"
    1.17 +Example "Diff_App-No.123a"
    1.18    Specification:
    1.19      Model:
    1.20        Given: \<open>Constants _\<close>
    1.21 @@ -86,11 +86,11 @@
    1.22  subsubsection \<open>Plain Example\<close>
    1.23  text \<open>
    1.24    This can occur in between text offering to start an interactive Calculation by using
    1.25 -  "Diff_App/No.123 a" as a link.
    1.26 +  "Diff_App-No.123a" as a link.
    1.27  \<close>
    1.28  text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
    1.29  
    1.30 -Example "Diff_App/No.123 a"
    1.31 +Example "Diff_App-No.123a"
    1.32  
    1.33         (* remove as soon as this ^^^ works as Isabelle/Isar commands ..*) \<close>
    1.34  
    1.35 @@ -102,7 +102,7 @@
    1.36  \<close>
    1.37  text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
    1.38  
    1.39 -Example "Diff_App/No.123 a"
    1.40 +Example "Diff_App-No.123a"
    1.41    Problem "univariate_calculus/Optimisation"
    1.42      Specification:
    1.43      Solution:
    1.44 @@ -119,7 +119,7 @@
    1.45  \<close>
    1.46  text \<open> (*.. remove as soon as this works as Isabelle/Isar commands ..*)
    1.47  
    1.48 -Example "Diff_App/No.123 a"
    1.49 +Example "Diff_App-No.123a"
    1.50    Problem "univariate_calculus/Optimisation"
    1.51      Specification:
    1.52        Model:
    1.53 @@ -193,7 +193,7 @@
    1.54    in the repository.
    1.55  
    1.56    The intermediate steps below will be deleted as soon as all above representations 
    1.57 -  of Example "Diff_App/No.123 a" work out.
    1.58 +  of Example "Diff_App-No.123a" work out.
    1.59  \<close>
    1.60  
    1.61  subsubsection \<open>Complete Specification at once\<close>