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 ( **)