export method parser;
authorwenzelm
Mon Mar 16 17:47:26 2009 +0100 (2009-03-16)
changeset 305458209a7196389
parent 30544 0ed8fe16331a
child 30546 b3b1f4184ae4
export method parser;
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Mar 16 17:46:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Mar 16 17:47:26 2009 +0100
     1.3 @@ -16,6 +16,8 @@
     1.4    val thin_tac: Proof.context -> string -> int -> tactic
     1.5    val subgoal_tac: Proof.context -> string -> int -> tactic
     1.6    val subgoals_tac: Proof.context -> string list -> int -> tactic
     1.7 +  val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     1.8 +    (thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
     1.9  end;
    1.10  
    1.11  signature RULE_INSTS =
    1.12 @@ -383,9 +385,7 @@
    1.13  
    1.14  (* rule_tac etc. -- refer to dynamic goal state! *)
    1.15  
    1.16 -local
    1.17 -
    1.18 -fun inst_meth inst_tac tac =
    1.19 +fun method inst_tac tac =
    1.20    Args.goal_spec --
    1.21    Scan.optional (Scan.lift
    1.22      (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
    1.23 @@ -397,15 +397,11 @@
    1.24          [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
    1.25        | _ => error "Cannot have instantiations with multiple rules")));
    1.26  
    1.27 -in
    1.28 -
    1.29 -val res_inst_meth = inst_meth res_inst_tac Tactic.resolve_tac;
    1.30 -val eres_inst_meth = inst_meth eres_inst_tac Tactic.eresolve_tac;
    1.31 -val cut_inst_meth = inst_meth cut_inst_tac Tactic.cut_rules_tac;
    1.32 -val dres_inst_meth = inst_meth dres_inst_tac Tactic.dresolve_tac;
    1.33 -val forw_inst_meth = inst_meth forw_inst_tac Tactic.forward_tac;
    1.34 -
    1.35 -end;
    1.36 +val res_inst_meth = method res_inst_tac Tactic.resolve_tac;
    1.37 +val eres_inst_meth = method eres_inst_tac Tactic.eresolve_tac;
    1.38 +val cut_inst_meth = method cut_inst_tac Tactic.cut_rules_tac;
    1.39 +val dres_inst_meth = method dres_inst_tac Tactic.dresolve_tac;
    1.40 +val forw_inst_meth = method forw_inst_tac Tactic.forward_tac;
    1.41  
    1.42  
    1.43  (* setup *)