src/Tools/isac/BridgeJEdit/Calculation.thy
changeset 60173 c2cc411ddc5f
parent 60171 f7060b6860cd
child 60174 21d482c9ab68
     1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 13:25:51 2021 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 15:22:39 2021 +0100
     1.3 @@ -11,7 +11,8 @@
     1.4  (** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)
     1.5  (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
     1.6  keywords
     1.7 -(** )"Example" :: thy_load (**) (isac_example) (** ) "spark_vc" :: thy_goal *)
     1.8 +(*WAS "Example" :: thy_load ("str")  ..in Isabelle2020*)
     1.9 +(** ) "Example" :: thy_load (isac_example) (*Unknown load command specification: "isac_example"*)
    1.10    and( **)"Problem" :: thy_decl (* root-problem + recursively in Solution;
    1.11                                 "spark_vc" :: thy_goal *)
    1.12    and "Specification" "Model" "References" :: diag
    1.13 @@ -122,7 +123,7 @@
    1.14  (** )
    1.15  val _ =                                                  
    1.16    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    1.17 -    (Resources.provide_parse_files "Example" -- Parse.parname
    1.18 +    (Resources.provide_parse_files (Command_Span.extensions ["str"]) -- Parse.parname
    1.19        >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    1.20          (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    1.21  ( **)