1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue Dec 08 13:39:52 2020 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue Dec 08 17:10:18 2020 +0100
     1.3 @@ -636,10 +636,23 @@
     1.4    | NONE => error ("There is no verification condition " ^
     1.5        quote vc_name ^ "."));
     1.6  \<close> ML \<open>
     1.7 +fun prefer_input ((inthy, inpbl : Problem.id), (thy, pbl)) met_id o_model =
     1.8 +  if inthy = thy andalso inpbl = pbl
     1.9 +  then ((thy, pbl, met_id) : References.T, o_model)
    1.10 +  else ((inthy, inpbl, Method.id_empty), [])
    1.11 +\<close> ML \<open>
    1.12 +(*  prove_vc : string -> Proof.context -> Proof.state*)
    1.13  fun prove_vc vc_name lthy =
    1.14    let
    1.15      val thy = Proof_Context.theory_of lthy;
    1.16      val (ctxt, stmt) = get_vc thy vc_name
    1.17 +(*//--------------------------------- new code --------------------------------\\*)
    1.18 +    val refs' = ("Biegelinie", ["Biegelinien"]) (*until Parse.name \<rightarrow> ParseC.problem_headline*)
    1.19 +    val (thy_id, pbl_id, met_id) = Refs_Data.get thy
    1.20 +    val (refs, o_model) = prefer_input (refs', (thy_id, pbl_id)) met_id (OMod_Data.get thy)
    1.21 +(*----------------------------------- new code ----------------------------------*)
    1.22 +    val _ = @{print} {a = "prove_vc", o_model = o_model, refs = refs}
    1.23 +(*\\--------------------------------- new code --------------------------------//*)
    1.24    in
    1.25      Specification.theorem true Thm.theoremK NONE
    1.26        (fn thmss => (Local_Theory.background_theory

     2.1 --- a/test/Tools/isac/Test_Some.thy	Tue Dec 08 13:39:52 2020 +0100
     2.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Dec 08 17:10:18 2020 +0100
     2.3 @@ -115,7 +115,29 @@
     2.4  *)
     2.5  spark_open \<open>~~/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d\<close>
     2.6  Problem procedure_g_c_d_4
     2.7 +(* WE GET DATA TRANSFERRED FROM Example ABOVE, OK..
     2.8  
     2.9 +{a = "prove_vc", o_model =
    2.10 + [(1, [1], "#Given", Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), [Free ("L", "real")]), (2, [1], "#Given", Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), [Free ("q_0", "real")]),
    2.11 +  (3, [1], "#Find", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]),
    2.12 +  (4, [1], "#Relate", Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"),
    2.13 +   [Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
    2.14 +      Const ("List.list.Nil", "bool list"),
    2.15 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Free ("y", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
    2.16 +      Const ("List.list.Nil", "bool list"),
    2.17 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("0", "real")) $ Free ("0", "real")) $
    2.18 +      Const ("List.list.Nil", "bool list"),
    2.19 +    Const ("List.list.Cons", "bool \<Rightarrow> bool list \<Rightarrow> bool list") $ (Const ("HOL.eq", "real \<Rightarrow> real \<Rightarrow> bool") $ (Const ("Biegelinie.M'_b", "real \<Rightarrow> real") $ Free ("L", "real")) $ Free ("0", "real")) $
    2.20 +      Const ("List.list.Nil", "bool list")]),
    2.21 +  (5, [1], "#undef", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
    2.22 +  (6, [1], "#undef", Const ("Biegelinie.GleichungsVariablen", "real list \<Rightarrow> una"),
    2.23 +   [Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c", "real") $ Const ("List.list.Nil", "real list"),
    2.24 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_2", "real") $ Const ("List.list.Nil", "real list"),
    2.25 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_3", "real") $ Const ("List.list.Nil", "real list"),
    2.26 +    Const ("List.list.Cons", "real \<Rightarrow> real list \<Rightarrow> real list") $ Free ("c_4", "real") $ Const ("List.list.Nil", "real list")]),
    2.27 +  (7, [1], "#undef", Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("dy", "real \<Rightarrow> real")])],
    2.28 + refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])} (line 654 of "~~/src/Tools/isac/BridgeJEdit/Calculation.thy")
    2.29 +*)
    2.30  ML \<open>
    2.31    (*
    2.32    AT ABOVE "ML" WE HAVE: