src/Tools/isac/BridgeJEdit/Calculation.thy
changeset 60508 ce09935439b3
parent 60505 137227934d2e
child 60513 cecbfe45f053
     1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Aug 03 18:06:02 2022 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Aug 03 18:17:27 2022 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    (**)"$ISABELLE_ISAC/MathEngine/MathEngine"
     1.5    (** )"SPARK_FDL"                             ( * remove after devel.of BridgeJEdit*)
     1.6  keywords "Example" :: thy_decl
     1.7 -and "Problem" "Specification" "Model" "References" "Solution" 
     1.8 +and "Specification" "Model" "References" "Solution" 
     1.9  
    1.10  begin
    1.11  
    1.12 @@ -198,15 +198,14 @@
    1.13  \<close> ML \<open>
    1.14  \<close> ML \<open>
    1.15  (*/----------------------------------------------------------------------------\*)
    1.16 -     Parse.name -- Parse.!!! (  \<^keyword>\<open>Problem\<close> |-- Parse.name -- 
    1.17 -       Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
    1.18 +     Parse.name -- Parse.!!! ( \<^keyword>\<open>Specification\<close> -- \<^keyword>\<open>:\<close> --
    1.19           \<^keyword>\<open>Model\<close> -- \<^keyword>\<open>:\<close>  |-- Problem.parse_model_input --
    1.20 -         Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input)))
    1.21 -: (string * (string * (Problem.model_input * references_input))) parser
    1.22 +         Parse.!!! ( \<^keyword>\<open>References\<close> -- \<^keyword>\<open>:\<close> |-- parse_references_input))
    1.23 +(*: (string * (Problem.model_input * references_input)) parser*)
    1.24  (*\----------------------------------------------------------------------------/*) 
    1.25  : Token.T list ->
    1.26  (*/----------------------------------------------------------------------------\*)
    1.27 -    (string * (string * (Problem.model_input * references_input)))
    1.28 +    (string * (Problem.model_input * references_input))
    1.29  (*\----------------------------------------------------------------------------/*)
    1.30  * Token.T list
    1.31  (*/----------------------------------------------------------------------------\* )