src/Pure/tctical.ML

 Tacticals
 *)
 
 infix 1 THEN THEN' THEN_BEST_FIRST;
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
+
+infix 0 THEN_ELSE;
 
 
 signature TACTICAL =
   sig
   structure Thm : THM

   val tapply		: tactic * thm -> thm Sequence.seq
   val THEN		: tactic * tactic -> tactic
   val THEN'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val THEN_BEST_FIRST	: tactic * ((thm->bool) * (thm->int) * tactic) 
 			  -> tactic
+  val THEN_ELSE		: tactic * (tactic*tactic) -> tactic
   val traced_tac	: (thm -> (thm * thm Sequence.seq) option) -> tactic
   val tracify		: bool ref -> tactic -> thm -> thm Sequence.seq
   val trace_BEST_FIRST	: bool ref
   val trace_DEPTH_FIRST	: bool ref
   val trace_REPEAT	: bool ref

 
 (*Like APPEND, but interleaves results of tac1 and tac2.*)
 fun (Tactic tf1)  INTLEAVE  (Tactic tf2) = 
   Tactic (fn state =>  Sequence.interleave(tf1 state,
                           Sequence.seqof(fn()=> Sequence.pull (tf2 state))));
+
+(*Conditional tactic.
+	tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
+	tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
+*)
+fun (Tactic tf) THEN_ELSE (Tactic tf1, Tactic tf2) = 
+  Tactic (fn state =>  
+    case Sequence.pull(tf state) of
+	None    => tf2 state		(*failed; try tactic 2*)
+      | seqcell => Sequence.flats 	(*succeeded; use tactic 1*)
+	            (Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell))));
+
 
 (*Versions for combining tactic-valued functions, as in
      SOMEGOAL (resolve_tac rls THEN' assume_tac) *)
 fun tac1 THEN' tac2 = fn x => tac1 x THEN tac2 x;
 fun tac1 ORELSE' tac2 = fn x => tac1 x ORELSE tac2 x;