--- 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 ***)