# HG changeset patch
# User lcp
# Date 783622994 -3600
# Node ID e0be228a9c5bfb319dd9d89db3cef4157730b50b
# Parent  ff4c6691de9d18be30d4f5e9ff96bf1c70044026
Pure/tctical/THEN_ELSE: new

diff -r ff4c6691de9d -r e0be228a9c5b src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Oct 31 18:01:02 1994 +0100
+++ b/src/Pure/tctical.ML	Mon Oct 31 18:03:14 1994 +0100
@@ -9,6 +9,8 @@
 infix 1 THEN THEN' THEN_BEST_FIRST;
 infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE';
 
+infix 0 THEN_ELSE;
+
 
 signature TACTICAL =
   sig
@@ -62,6 +64,7 @@
   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
@@ -124,6 +127,18 @@
   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;