# HG changeset patch # User wenzelm # Date 1170023356 -3600 # Node ID 0544af1a5117b0f9ab766a9ec3cff55cd3d5c58c # Parent 6fe46a7259ec49e8a53fd3e3fa3d5dfe3f1ec2a4 added simproc_setup; diff -r 6fe46a7259ec -r 0544af1a5117 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Jan 28 23:29:15 2007 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sun Jan 28 23:29:16 2007 +0100 @@ -20,6 +20,7 @@ val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory val declaration: string -> local_theory -> local_theory + val simproc_setup: string * string list * string -> local_theory -> local_theory val have: ((string * Attrib.src list) * (string * string list) list) list -> bool -> Proof.state -> Proof.state val hence: ((string * Attrib.src list) * (string * string list) list) list -> @@ -238,6 +239,16 @@ #> Context.proof_map; +(* simprocs *) + +fun simproc_setup (name, pats, proc) = + ML_Context.use_let + "val simproc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option" + ("Context.map_proof (Simplifier.def_simproc " ^ ML_Syntax.print_string name ^ " " ^ + ML_Syntax.print_list ML_Syntax.print_string pats ^ " simproc)") proc + |> Context.proof_map; + + (* goals *) fun goal opt_chain goal stmt int = diff -r 6fe46a7259ec -r 0544af1a5117 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sun Jan 28 23:29:15 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Sun Jan 28 23:29:16 2007 +0100 @@ -311,6 +311,12 @@ (P.opt_target -- P.text >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); +val simproc_setupP = + OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) + (P.opt_target -- + P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text + >> (fn (((loc, x), y), z) => Toplevel.local_theory loc (IsarCmd.simproc_setup (x, y, z)))); + (* translation functions *) @@ -929,9 +935,10 @@ constdefsP, definitionP, abbreviationP, notationP, axiomatizationP, theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP, declarationP, - parse_ast_translationP, parse_translationP, print_translationP, - typed_print_translationP, print_ast_translationP, - token_translationP, oracleP, contextP, localeP, + simproc_setupP, parse_ast_translationP, parse_translationP, + print_translationP, typed_print_translationP, + print_ast_translationP, token_translationP, oracleP, contextP, + localeP, (*proof commands*) theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP, assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,