1.1 --- a/src/Tools/isac/Specify/i-model.sml	Wed Apr 05 17:46:25 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sat Apr 29 15:53:37 2023 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4  
     1.5    type T
     1.6    type T_TEST
     1.7 +  val OLD_to_TEST: T -> T_TEST
     1.8    val empty: T
     1.9    val empty_TEST: T_TEST
    1.10    type single
    1.11 @@ -33,6 +34,7 @@
    1.12    val single_to_string_TEST: Proof.context -> single_TEST -> string
    1.13    val to_string: Proof.context -> T -> string
    1.14    val to_string_TEST: Proof.context -> T_TEST -> string
    1.15 +  val feedback_OLD_to_TEST: feedback -> feedback_TEST
    1.16  
    1.17    datatype add_single = Add of single | Err of string
    1.18    val init: Model_Pattern.T -> T

     2.1 --- a/src/Tools/isac/Specify/p-spec.sml	Wed Apr 05 17:46:25 2023 +0200
     2.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Sat Apr 29 15:53:37 2023 +0200
     2.3 @@ -208,7 +208,7 @@
     2.4    | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
     2.5    | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))
     2.6    | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 
     2.7 -    raise ERROR ("parsitm (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
     2.8 +    raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
     2.9  
    2.10  fun imodel2fstr iitems = 
    2.11    let 

     3.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Wed Apr 05 17:46:25 2023 +0200
     3.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Sat Apr 29 15:53:37 2023 +0200
     3.3 @@ -392,8 +392,30 @@
     3.4  text \<open>
     3.5    # 7: xxxxx:
     3.6  \<close> 
     3.7 -ML \<open> (* # 7: ISAC suggests a next step on request *)
     3.8 +ML \<open> (* # 7: user inputs value of Method_Ref, which shows the respective Model *)
     3.9  \<close>
    3.10 +
    3.11 +subsubsection \<open>Specification with Model for the Method_Ref\<close>
    3.12 +
    3.13 +text \<open>
    3.14 +  Observe the (still outcommented) toggles \<Odot>\<Otimes> changed according to the Reference
    3.15 +\<close>
    3.16 +Example_TEST "Diff_App-No.123a" (*Specification of the Method_Ref*)
    3.17 +  Specification:
    3.18 +    Model:        
    3.19 +      Given: \<open>Constants [r = 7]\<close> \<open>Maximum A\<close> \<open>AdditionalValues [u, v]\<close>
    3.20 +        \<open>Extremum (A = 2 * u * v - u \<up> 2)\<close>
    3.21 +        \<open>SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\<close>
    3.22 +        \<open>FunctionVariable u\<close> \<open>Domain {0 <..< r}\<close> \<open>ErrorBound (\<epsilon> = 0)\<close> 
    3.23 +      Where: \<open>0 < r\<close>
    3.24 +      Find: \<open>Results (A, u, v)\<close>
    3.25 +      Relate:
    3.26 +    References:
    3.27 +      Theory_Ref: "Diff_App"
    3.28 +  (*\<Odot>*) Problem_Ref: "univariate_calculus/Optimisation"
    3.29 +  (*\<Otimes>*) Method_Ref: "Optimisation/by_univariate_calculus"
    3.30 +(*Solution:*)
    3.31 +
    3.32  text \<open> --- remove this line and make content Isar input---\
    3.33  ---------- remove this line and make content Isar input---/
    3.34  \<close>