src/Pure/Isar/context_rules.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18874 05585eee8d74
     1.1 --- a/src/Pure/Isar/context_rules.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Declarations of intro/elim/dest rules in Pure; see
     1.8 -Provers/classical.ML for a more specialized version of the same idea.
     1.9 +Declarations of intro/elim/dest rules in Pure (see also
    1.10 +Provers/classical.ML for a more specialized version of the same idea).
    1.11  *)
    1.12  
    1.13  signature CONTEXT_RULES =
    1.14 @@ -20,18 +20,19 @@
    1.15    val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.16    val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    1.17    val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    1.18 -  val intro_bang: int option -> Context.generic attribute
    1.19 -  val elim_bang: int option -> Context.generic attribute
    1.20 -  val dest_bang: int option -> Context.generic attribute
    1.21 -  val intro: int option -> Context.generic attribute
    1.22 -  val elim: int option -> Context.generic attribute
    1.23 -  val dest: int option -> Context.generic attribute
    1.24 -  val intro_query: int option -> Context.generic attribute
    1.25 -  val elim_query: int option -> Context.generic attribute
    1.26 -  val dest_query: int option -> Context.generic attribute
    1.27 -  val rule_del: Context.generic attribute
    1.28 -  val add_args: (int option -> 'a attribute) -> (int option -> 'a attribute) ->
    1.29 -    (int option -> 'a attribute) -> Attrib.src -> 'a attribute
    1.30 +  val intro_bang: int option -> attribute
    1.31 +  val elim_bang: int option -> attribute
    1.32 +  val dest_bang: int option -> attribute
    1.33 +  val intro: int option -> attribute
    1.34 +  val elim: int option -> attribute
    1.35 +  val dest: int option -> attribute
    1.36 +  val intro_query: int option -> attribute
    1.37 +  val elim_query: int option -> attribute
    1.38 +  val dest_query: int option -> attribute
    1.39 +  val rule_del: attribute
    1.40 +  val add_args:
    1.41 +    (int option -> attribute) -> (int option -> attribute) -> (int option -> attribute) ->
    1.42 +    Attrib.src -> attribute
    1.43  end;
    1.44  
    1.45  structure ContextRules: CONTEXT_RULES =
    1.46 @@ -166,7 +167,7 @@
    1.47  (* wrappers *)
    1.48  
    1.49  fun gen_add_wrapper upd w =
    1.50 -  Context.map_theory (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.51 +  Context.theory_map (Rules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) =>
    1.52      make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)));
    1.53  
    1.54  val addSWrapper = gen_add_wrapper Library.apfst;
    1.55 @@ -203,7 +204,7 @@
    1.56  val dest_query  = rule_add elim_queryK Tactic.make_elim;
    1.57  
    1.58  val _ = Context.add_setup
    1.59 -  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
    1.60 +  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [intro_query NONE])]);
    1.61  
    1.62  
    1.63  (* concrete syntax *)
    1.64 @@ -213,13 +214,10 @@
    1.65      >> (fn (f, n) => f n)) x;
    1.66  
    1.67  val rule_atts =
    1.68 - [("intro", Attrib.common (add_args intro_bang intro intro_query),
    1.69 -    "declaration of introduction rule"),
    1.70 -  ("elim", Attrib.common (add_args elim_bang elim elim_query),
    1.71 -    "declaration of elimination rule"),
    1.72 -  ("dest", Attrib.common (add_args dest_bang dest dest_query),
    1.73 -    "declaration of destruction rule"),
    1.74 -  ("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
    1.75 + [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),
    1.76 +  ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"),
    1.77 +  ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"),
    1.78 +  ("rule", Attrib.syntax (Scan.lift Args.del >> K rule_del),
    1.79      "remove declaration of intro/elim/dest rule")];
    1.80  
    1.81  val _ = Context.add_setup (Attrib.add_attributes rule_atts);