tuned
authorwneuper <Walther.Neuper@jku.at>
Thu, 04 Aug 2022 15:25:44 +0200
changeset 60513cecbfe45f053
parent 60512 eee69d41805c
child 60514 19bd2f740479
tuned
src/Tools/isac/BridgeJEdit/Calculation.thy
     1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Aug 04 15:24:58 2022 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Aug 04 15:25:44 2022 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4    Parse.!!! ( \<^keyword>\<open>Problem_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name --
     1.5    Parse.!!! ( \<^keyword>\<open>Method_Ref\<close> -- \<^keyword>\<open>Theory_Ref\<close> |-- Parse.name)))
     1.6  \<close> ML \<open>
     1.7 -parse_references_input: references_input parser (*TODO: dpes not yet work,
     1.8 +parse_references_input: references_input parser (*TODO: does not yet work,
     1.9    thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
    1.10  \<close> ML \<open>
    1.11  op --  : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
    1.12 @@ -154,6 +154,7 @@
    1.13  \<close> ML \<open>
    1.14  \<close> ML \<open>
    1.15  \<close> ML \<open>
    1.16 +(* but       "<markup>" would be required as an argument *)
    1.17  fun is_empty str = 
    1.18    let
    1.19      val strl = Symbol.explode str |> rev