summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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 =