summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | oheimb |

Fri, 23 Oct 1998 20:34:59 +0200 | |

changeset 5754 | 98744e38ded1 |

parent 5753 | c90b5f7d0c61 |

child 5755 | 22081de41254 |

added SOLVE tactical

doc-src/Ref/tctical.tex | file | annotate | diff | comparison | revisions | |

src/Pure/search.ML | file | annotate | diff | comparison | revisions |

--- a/doc-src/Ref/tctical.tex Fri Oct 23 20:28:33 1998 +0200 +++ b/doc-src/Ref/tctical.tex Fri Oct 23 20:34:59 1998 +0200 @@ -254,6 +254,7 @@ \begin{ttbox} COND : (thm->bool) -> tactic -> tactic -> tactic IF_UNSOLVED : tactic -> tactic +SOLVE : tactic -> tactic DETERM : tactic -> tactic \end{ttbox} \begin{ttdescription} @@ -268,6 +269,10 @@ returns the proof state otherwise. Many common tactics, such as {\tt resolve_tac}, fail if applied to a proof state that has no subgoals. +\item[\ttindexbold{SOLVE} {\it tac}] +applies {\it tac\/} to the proof state and then fails iff there are subgoals +left. + \item[\ttindexbold{DETERM} {\it tac}] applies {\it tac\/} to the proof state and returns the head of the resulting sequence. {\tt DETERM} limits the search space by making its

--- a/src/Pure/search.ML Fri Oct 23 20:28:33 1998 +0200 +++ b/src/Pure/search.ML Fri Oct 23 20:34:59 1998 +0200 @@ -23,6 +23,7 @@ val has_fewer_prems : int -> thm -> bool val IF_UNSOLVED : tactic -> tactic + val SOLVE : tactic -> tactic val trace_BEST_FIRST : bool ref val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic @@ -65,6 +66,9 @@ (*Apply a tactic if subgoals remain, else do nothing.*) val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; +(*Force a tactic to solve its goal completely, otherwise fail *) +fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac; + (*Execute tac1, but only execute tac2 if there are at least as many subgoals as before. This ensures that tac2 is only applied to an outcome of tac1.*) fun (tac1 THEN_MAYBE tac2) st =