src/Pure/Isar/isar_syn.ML
changeset 22202 0544af1a5117
parent 22117 505e040bdcdb
child 22239 9ddd3349d597
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:15 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:16 2007 +0100
     1.3 @@ -311,6 +311,12 @@
     1.4      (P.opt_target -- P.text
     1.5      >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
     1.6  
     1.7 +val simproc_setupP =
     1.8 +  OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     1.9 +    (P.opt_target --
    1.10 +      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text
    1.11 +    >> (fn (((loc, x), y), z) => Toplevel.local_theory loc (IsarCmd.simproc_setup (x, y, z))));
    1.12 +
    1.13  
    1.14  (* translation functions *)
    1.15  
    1.16 @@ -929,9 +935,10 @@
    1.17    constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
    1.18    theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
    1.19    ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
    1.20 -  parse_ast_translationP, parse_translationP, print_translationP,
    1.21 -  typed_print_translationP, print_ast_translationP,
    1.22 -  token_translationP, oracleP, contextP, localeP,
    1.23 +  simproc_setupP, parse_ast_translationP, parse_translationP,
    1.24 +  print_translationP, typed_print_translationP,
    1.25 +  print_ast_translationP, token_translationP, oracleP, contextP,
    1.26 +  localeP,
    1.27    (*proof commands*)
    1.28    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.29    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,