1.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Jun 14 09:46:35 2005 +0200
     1.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue Jun 14 21:56:55 2005 +0200
     1.3 @@ -18,6 +18,7 @@
     1.4    val make: bool -> term option -> Sign.sg * term -> string list -> (string * T option) list
     1.5    val rename_params: string list list -> thm -> thm
     1.6    val params: string list list -> 'a attribute
     1.7 +  type tactic
     1.8  end;
     1.9  
    1.10  structure RuleCases: RULE_CASES =
    1.11 @@ -138,4 +139,9 @@
    1.12  
    1.13  fun params xss = Drule.rule_attribute (K (rename_params xss));
    1.14  
    1.15 +
    1.16 +(* tactics with cases *)
    1.17 +
    1.18 +type tactic = thm -> (thm * (string * T option) list) Seq.seq;
    1.19 +
    1.20  end;