RuleCases.make opaq;
authorwenzelm
Thu Jul 13 11:39:41 2000 +0200 (2000-07-13)
changeset 92949ecb78a8d471
parent 9293 3da2533e0a61
child 9295 5fc3c1f84e8a
RuleCases.make opaq;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jul 13 11:39:22 2000 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 13 11:39:41 2000 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4    val multi_resolve: thm list -> thm -> thm Seq.seq
     1.5    val multi_resolves: thm list -> thm list -> thm Seq.seq
     1.6    val resolveq_tac: thm Seq.seq -> int -> tactic
     1.7 -  val resolveq_cases_tac: (thm * string list) Seq.seq
     1.8 +  val resolveq_cases_tac: bool -> (thm * string list) Seq.seq
     1.9      -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
    1.10    val rule_tac: thm list -> thm list -> int -> tactic
    1.11    val rule: thm list -> Proof.method
    1.12 @@ -273,8 +273,8 @@
    1.13  
    1.14  val resolveq_tac = gen_resolveq_tac Tactic.rtac;
    1.15  
    1.16 -val resolveq_cases_tac = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
    1.17 -  Seq.map (rpair (RuleCases.make rule cases)) (Tactic.rtac rule i st));
    1.18 +fun resolveq_cases_tac opaq = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
    1.19 +  Seq.map (rpair (RuleCases.make opaq rule cases)) (Tactic.rtac rule i st));
    1.20  
    1.21  
    1.22  (* simple rule *)