pwd test by WN
authorWalther Neuper <walther.neuper@jku.at>
Wed, 07 Apr 2021 21:33:01 +0200
changeset 601854244e4b5e124
parent 60184 4dbc18d4a1dd
child 60186 a81828f24172
pwd test by WN
src/Tools/isac/BridgeJEdit/Calculation.thy
     1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Tue Apr 06 15:52:27 2021 +0200
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Apr 07 21:33:01 2021 +0200
     1.3 @@ -146,6 +146,10 @@
     1.4    Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"
     1.5      ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))
     1.6  \<close> ML \<open>
     1.7 +fun dummy2 _ (thy: theory) = thy
     1.8 +\<close> ML \<open> (*or*)
     1.9 +fun dummy2 _ (ctxt: Proof.context) = ctxt
    1.10 +\<close> ML \<open>
    1.11  val _ =
    1.12    Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy"
    1.13      ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))