# HG changeset patch
# User wenzelm
# Date 1118779015 -7200
# Node ID 305ce441869d337322a4df67f40fefe445341253
# Parent  48832eba5b1ef6873e59c0a01b420bb42ca78dd8
added type tactic;

diff -r 48832eba5b1e -r 305ce441869d src/Pure/Isar/rule_cases.ML
--- 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;