--- 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;