module now right after ProofContext (for locales);
authorwenzelm
Tue Jul 16 18:39:27 2002 +0200 (2002-07-16 ago)
changeset 1337218790d503fe0
parent 13371 82a057cf4413
child 13373 33b7736d8cc0
module now right after ProofContext (for locales);
src/Pure/Isar/context_rules.ML
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue Jul 16 18:38:36 2002 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue Jul 16 18:39:27 2002 +0200
     1.3 @@ -11,17 +11,17 @@
     1.4  sig
     1.5    type netpair
     1.6    type T
     1.7 -  val netpair_bang: Proof.context -> netpair
     1.8 -  val netpair: Proof.context -> netpair
     1.9 +  val netpair_bang: ProofContext.context -> netpair
    1.10 +  val netpair: ProofContext.context -> netpair
    1.11    val orderlist: ((int * int) * 'a) list -> 'a list
    1.12    val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list
    1.13 -  val find_rules: bool -> thm list -> term -> Proof.context -> thm list list
    1.14 +  val find_rules: bool -> thm list -> term -> ProofContext.context -> thm list list
    1.15    val print_global_rules: theory -> unit
    1.16 -  val print_local_rules: Proof.context -> unit
    1.17 +  val print_local_rules: ProofContext.context -> unit
    1.18    val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.19    val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory
    1.20 -  val Swrap: Proof.context -> (int -> tactic) -> int -> tactic
    1.21 -  val wrap: Proof.context -> (int -> tactic) -> int -> tactic
    1.22 +  val Swrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    1.23 +  val wrap: ProofContext.context -> (int -> tactic) -> int -> tactic
    1.24    val intro_bang_global: int option -> theory attribute
    1.25    val elim_bang_global: int option -> theory attribute
    1.26    val dest_bang_global: int option -> theory attribute
    1.27 @@ -32,24 +32,24 @@
    1.28    val elim_query_global: int option -> theory attribute
    1.29    val dest_query_global: int option -> theory attribute
    1.30    val rule_del_global: theory attribute
    1.31 -  val intro_bang_local: int option -> Proof.context attribute
    1.32 -  val elim_bang_local: int option -> Proof.context attribute
    1.33 -  val dest_bang_local: int option -> Proof.context attribute
    1.34 -  val intro_local: int option -> Proof.context attribute
    1.35 -  val elim_local: int option -> Proof.context attribute
    1.36 -  val dest_local: int option -> Proof.context attribute
    1.37 -  val intro_query_local: int option -> Proof.context attribute
    1.38 -  val elim_query_local: int option -> Proof.context attribute
    1.39 -  val dest_query_local: int option -> Proof.context attribute
    1.40 -  val rule_del_local: Proof.context attribute
    1.41 +  val intro_bang_local: int option -> ProofContext.context attribute
    1.42 +  val elim_bang_local: int option -> ProofContext.context attribute
    1.43 +  val dest_bang_local: int option -> ProofContext.context attribute
    1.44 +  val intro_local: int option -> ProofContext.context attribute
    1.45 +  val elim_local: int option -> ProofContext.context attribute
    1.46 +  val dest_local: int option -> ProofContext.context attribute
    1.47 +  val intro_query_local: int option -> ProofContext.context attribute
    1.48 +  val elim_query_local: int option -> ProofContext.context attribute
    1.49 +  val dest_query_local: int option -> ProofContext.context attribute
    1.50 +  val rule_del_local: ProofContext.context attribute
    1.51    val addXIs_global: theory * thm list -> theory
    1.52    val addXEs_global: theory * thm list -> theory
    1.53    val addXDs_global: theory * thm list -> theory
    1.54    val delrules_global: theory * thm list -> theory
    1.55 -  val addXIs_local: Proof.context * thm list -> Proof.context
    1.56 -  val addXEs_local: Proof.context * thm list -> Proof.context
    1.57 -  val addXDs_local: Proof.context * thm list -> Proof.context
    1.58 -  val delrules_local: Proof.context * thm list -> Proof.context
    1.59 +  val addXIs_local: ProofContext.context * thm list -> ProofContext.context
    1.60 +  val addXEs_local: ProofContext.context * thm list -> ProofContext.context
    1.61 +  val addXDs_local: ProofContext.context * thm list -> ProofContext.context
    1.62 +  val delrules_local: ProofContext.context * thm list -> ProofContext.context
    1.63    val setup: (theory -> theory) list
    1.64  end;
    1.65  
    1.66 @@ -264,37 +264,11 @@
    1.67  val delrules_local = modifier rule_del_local;
    1.68  
    1.69  
    1.70 -(* concrete syntax *)
    1.71 -
    1.72 -fun add_args a b c x = Attrib.syntax
    1.73 -  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
    1.74 -    >> (fn (f, n) => f n)) x;
    1.75 -
    1.76 -fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
    1.77 -
    1.78 -
    1.79 -val rule_atts =
    1.80 - [("intro",
    1.81 -   (add_args intro_bang_global intro_global intro_query_global,
    1.82 -    add_args intro_bang_local intro_local intro_query_local),
    1.83 -    "declaration of introduction rule"),
    1.84 -  ("elim",
    1.85 -   (add_args elim_bang_global elim_global elim_query_global,
    1.86 -    add_args elim_bang_local elim_local elim_query_local),
    1.87 -    "declaration of elimination rule"),
    1.88 -  ("dest",
    1.89 -   (add_args dest_bang_global dest_global dest_query_global,
    1.90 -    add_args dest_bang_local dest_local dest_query_local),
    1.91 -    "declaration of destruction rule"),
    1.92 -  ("rule", (del_args rule_del_global, del_args rule_del_local),
    1.93 -    "remove declaration of intro/elim/dest rule")];
    1.94 -
    1.95 -
    1.96  
    1.97  (** theory setup **)
    1.98  
    1.99  val setup =
   1.100 - [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts];
   1.101 + [GlobalRules.init, LocalRules.init];
   1.102  
   1.103  
   1.104  end;