1.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Fri Mar 12 15:22:39 2021 +0100
     1.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Mar 15 10:04:17 2021 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory Boogie
     1.6  imports Main
     1.7 +(*WAS    "boogie_file" :: thy_load ("b2i") *)
     1.8  keywords "boogie_file" :: thy_load
     1.9  begin
    1.10  
    1.11 @@ -58,12 +59,14 @@
    1.12  external_file \<open>Boogie_Max.certs\<close>
    1.13  declare [[smt_certificates = "Boogie_Max.certs"]]
    1.14  
    1.15 +(*WAS       \<open>Boogie_Max\<close> *)
    1.16  boogie_file \<open>Boogie_Max.b2i\<close>
    1.17  
    1.18  
    1.19  external_file \<open>Boogie_Dijkstra.certs\<close>
    1.20  declare [[smt_certificates = "Boogie_Dijkstra.certs"]]
    1.21  
    1.22 +(*WAS       \<open>Boogie_Dijkstra\<close> *)
    1.23  boogie_file \<open>Boogie_Dijkstra.b2i\<close>
    1.24  
    1.25  
    1.26 @@ -71,6 +74,7 @@
    1.27  external_file \<open>VCC_Max.certs\<close>
    1.28  declare [[smt_certificates = "VCC_Max.certs"]]
    1.29  
    1.30 +(*WAS       \<open>VCC_Max\<close> *)
    1.31  boogie_file \<open>VCC_Max.b2i\<close>
    1.32  
    1.33  end

     2.1 --- a/src/HOL/SMT_Examples/boogie.ML	Fri Mar 12 15:22:39 2021 +0100
     2.2 +++ b/src/HOL/SMT_Examples/boogie.ML	Mon Mar 15 10:04:17 2021 +0100
     2.3 @@ -265,6 +265,17 @@
     2.4  
     2.5  (* Isar command *)
     2.6  
     2.7 +(*WAS in Isabelle2020
     2.8 +val _ =
     2.9 +  Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close>
    2.10 +    "prove verification condition from .b2i file"
    2.11 +    (Resources.provide_parse_files "boogie_file" >> (fn files =>
    2.12 +      Toplevel.theory (fn thy =>
    2.13 +        let
    2.14 +          val ([{lines, ...}], thy') = files thy;
    2.15 +          val _ = boogie_prove thy' lines;
    2.16 +        in thy' end)))
    2.17 +*)
    2.18  val _ =
    2.19    Outer_Syntax.command \<^command_keyword>\<open>boogie_file\<close>
    2.20      "prove verification condition from .b2i file"

     3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 15:22:39 2021 +0100
     3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 15 10:04:17 2021 +0100
     3.3 @@ -12,8 +12,8 @@
     3.4  (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
     3.5  keywords
     3.6  (*WAS "Example" :: thy_load ("str")  ..in Isabelle2020*)
     3.7 -(** ) "Example" :: thy_load (isac_example) (*Unknown load command specification: "isac_example"*)
     3.8 -  and( **)"Problem" :: thy_decl (* root-problem + recursively in Solution;
     3.9 +(**) "Example" :: thy_load (*(isac_example) ..would involve registering in Isabelle/Scala*)
    3.10 +  and(**)"Problem" :: thy_decl (* root-problem + recursively in Solution;
    3.11                                 "spark_vc" :: thy_goal *)
    3.12    and "Specification" "Model" "References" :: diag
    3.13      (*TRIED: diag quasi_command qed_script thy_decl thy_defn thy_goal thy_goal_stmt thy_stmt vvv *)
    3.14 @@ -120,13 +120,13 @@
    3.15  section \<open>setup command_keyword + preliminary test\<close>
    3.16  ML \<open>                                            
    3.17  \<close> ML \<open>
    3.18 -(** )
    3.19 +(**)
    3.20  val _ =                                                  
    3.21    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    3.22 -    (Resources.provide_parse_files (Command_Span.extensions ["str"]) -- Parse.parname
    3.23 +    (Resources.provide_parse_files (Command_Span.extensions [""]) -- Parse.parname
    3.24        >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    3.25          (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    3.26 -( **)
    3.27 +(**)
    3.28  \<close> ML \<open>
    3.29  (Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation))
    3.30  :
    3.31 @@ -225,10 +225,10 @@
    3.32  \<close> ML \<open>
    3.33  \<close>
    3.34  
    3.35 -subsection \<open>test runs with test-Example\<close>
    3.36 -(** )
    3.37 -Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    3.38 -( **)
    3.39 +subsection \<open>runs with test-Example\<close>
    3.40 +(**)
    3.41 +Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70.str\<close>
    3.42 +(**)
    3.43  Problem ("Biegelinie", ["Biegelinien"])
    3.44  (*1 collapse* )
    3.45    Specification: