equal
deleted
inserted
replaced
323 Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl) |
323 Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl) |
324 (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text) |
324 (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text) |
325 >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); |
325 >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); |
326 |
326 |
327 val _ = |
327 val _ = |
328 Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl) |
328 Outer_Syntax.local_theory "declaration" "generic ML declaration" |
329 (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration); |
329 (Keyword.tag_ml Keyword.thy_decl) |
|
330 (Parse.opt_keyword "pervasive" -- Parse.ML_source |
|
331 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); |
|
332 |
|
333 val _ = |
|
334 Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration" |
|
335 (Keyword.tag_ml Keyword.thy_decl) |
|
336 (Parse.opt_keyword "pervasive" -- Parse.ML_source |
|
337 >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); |
330 |
338 |
331 val _ = |
339 val _ = |
332 Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl) |
340 Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl) |
333 (Parse.name -- |
341 (Parse.name -- |
334 (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") -- |
342 (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") -- |