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

author | paulson |

Wed, 23 Jul 1997 11:48:59 +0200 | |

changeset 3561 | 329441e7eeee |

parent 3560 | 7db9a44dfa06 |

child 3562 | 5380acac8c83 |

Removal of tactical STATE

NEWS | file | annotate | diff | comparison | revisions | |

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

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

--- a/NEWS Wed Jul 23 11:11:14 1997 +0200 +++ b/NEWS Wed Jul 23 11:48:59 1997 +0200 @@ -13,6 +13,9 @@ * improved output of warnings / errors; +* deleted the obsolete tactical STATE, which was declared by + fun STATE tacfun st = tacfun st st; + New in Isabelle94-8 (May 1997) ------------------------------

--- a/doc-src/Ref/tactic.tex Wed Jul 23 11:11:14 1997 +0200 +++ b/doc-src/Ref/tactic.tex Wed Jul 23 11:48:59 1997 +0200 @@ -564,31 +564,23 @@ really need to code tactics from scratch. \subsection{Operations on type {\tt tactic}} -\index{tactics!primitives for coding} -A tactic maps theorems to theorem sequences (lazy lists). The type -constructor for sequences is called \mltydx{Sequence.seq}. To simplify the -types of tactics and tacticals, Isabelle defines a type abbreviations: +\index{tactics!primitives for coding} A tactic maps theorems to sequences of +theorems. The type constructor for sequences (lazy lists) is called +\mltydx{Sequence.seq}. To simplify the types of tactics and tacticals, +Isabelle defines a type abbreviation: \begin{ttbox} type tactic = thm -> thm Sequence.seq \end{ttbox} The following operations provide means for coding tactics in a clean style. \begin{ttbox} PRIMITIVE : (thm -> thm) -> tactic -STATE : (thm -> tactic) -> tactic SUBGOAL : ((term*int) -> tactic) -> int -> tactic \end{ttbox} \begin{ttdescription} -\item[\ttindexbold{PRIMITIVE} $f$] -applies $f$ to the proof state and returns the result as a -one-element sequence. This packages the meta-rule~$f$ as a tactic. - -\item[\ttindexbold{STATE} $f$] -applies $f$ to the proof state and then applies the resulting tactic to the -same state. It supports the following style, where the tactic body is -expressed using tactics and tacticals, but may peek at the proof state: -\begin{ttbox} -STATE (fn state => {\it tactic-valued expression}) -\end{ttbox} +\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that + applies $f$ to the proof state and returns the result as a one-element + sequence. If $f$ raises an exception, then the tactic's result is the empty + sequence. \item[\ttindexbold{SUBGOAL} $f$ $i$] extracts subgoal~$i$ from the proof state as a term~$t$, and computes a

--- a/src/Pure/tctical.ML Wed Jul 23 11:11:14 1997 +0200 +++ b/src/Pure/tctical.ML Wed Jul 23 11:48:59 1997 +0200 @@ -49,7 +49,6 @@ val REPEAT_SOME : (int -> tactic) -> tactic val SELECT_GOAL : tactic -> int -> tactic val SOMEGOAL : (int -> tactic) -> tactic - val STATE : (thm -> tactic) -> tactic val strip_context : term -> (string * typ) list * term list * term val SUBGOAL : ((term*int) -> tactic) -> int -> tactic val suppress_tracing : bool ref @@ -75,9 +74,6 @@ type tactic = thm -> thm Sequence.seq; -(*Makes a tactic from one that uses the components of the state.*) -fun STATE tacfun st = tacfun st st; - (*** LCF-style tacticals ***)