src/Pure/search.ML
changeset 8149 941afb897532
parent 5956 ab4d13e9e77a
child 9094 530e7a33b3dd
     1.1 --- a/src/Pure/search.ML	Fri Jan 28 11:22:02 2000 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Jan 28 11:23:41 2000 +0100
     1.3 @@ -24,6 +24,7 @@
     1.4    val has_fewer_prems	: int -> thm -> bool   
     1.5    val IF_UNSOLVED	: tactic -> tactic
     1.6    val SOLVE		: tactic -> tactic
     1.7 +  val DETERM_UNTIL_SOLVED: tactic -> tactic
     1.8    val trace_BEST_FIRST	: bool ref
     1.9    val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    1.10    val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    1.11 @@ -69,6 +70,9 @@
    1.12  (*Force a tactic to solve its goal completely, otherwise fail *)
    1.13  fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
    1.14  
    1.15 +(*Force repeated application of tactic until goal is solved completely *)
    1.16 +val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1);
    1.17 +
    1.18  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    1.19    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    1.20  fun (tac1 THEN_MAYBE tac2) st =