added type tactic;

--- a/src/Pure/Isar/rule_cases.ML	Tue Jun 14 09:46:35 2005 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Tue Jun 14 21:56:55 2005 +0200
@@ -18,6 +18,7 @@
   val make: bool -> term option -> Sign.sg * term -> string list -> (string * T option) list
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
+  type tactic
 end;
 
 structure RuleCases: RULE_CASES =
@@ -138,4 +139,9 @@
 
 fun params xss = Drule.rule_attribute (K (rename_params xss));
 
+
+(* tactics with cases *)
+
+type tactic = thm -> (thm * (string * T option) list) Seq.seq;
+
 end;