author | paulson |

Wed Jul 23 11:48:59 1997 +0200 (1997-07-23) | |

changeset 3561 | 329441e7eeee |

parent 3560 | 7db9a44dfa06 |

child 3562 | 5380acac8c83 |

Removal of tactical STATE

NEWS | file | annotate | diff | revisions | |

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

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

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

2.1 --- a/doc-src/Ref/tactic.tex Wed Jul 23 11:11:14 1997 +0200 2.2 +++ b/doc-src/Ref/tactic.tex Wed Jul 23 11:48:59 1997 +0200 2.3 @@ -564,31 +564,23 @@ 2.4 really need to code tactics from scratch. 2.5 2.6 \subsection{Operations on type {\tt tactic}} 2.7 -\index{tactics!primitives for coding} 2.8 -A tactic maps theorems to theorem sequences (lazy lists). The type 2.9 -constructor for sequences is called \mltydx{Sequence.seq}. To simplify the 2.10 -types of tactics and tacticals, Isabelle defines a type abbreviations: 2.11 +\index{tactics!primitives for coding} A tactic maps theorems to sequences of 2.12 +theorems. The type constructor for sequences (lazy lists) is called 2.13 +\mltydx{Sequence.seq}. To simplify the types of tactics and tacticals, 2.14 +Isabelle defines a type abbreviation: 2.15 \begin{ttbox} 2.16 type tactic = thm -> thm Sequence.seq 2.17 \end{ttbox} 2.18 The following operations provide means for coding tactics in a clean style. 2.19 \begin{ttbox} 2.20 PRIMITIVE : (thm -> thm) -> tactic 2.21 -STATE : (thm -> tactic) -> tactic 2.22 SUBGOAL : ((term*int) -> tactic) -> int -> tactic 2.23 \end{ttbox} 2.24 \begin{ttdescription} 2.25 -\item[\ttindexbold{PRIMITIVE} $f$] 2.26 -applies $f$ to the proof state and returns the result as a 2.27 -one-element sequence. This packages the meta-rule~$f$ as a tactic. 2.28 - 2.29 -\item[\ttindexbold{STATE} $f$] 2.30 -applies $f$ to the proof state and then applies the resulting tactic to the 2.31 -same state. It supports the following style, where the tactic body is 2.32 -expressed using tactics and tacticals, but may peek at the proof state: 2.33 -\begin{ttbox} 2.34 -STATE (fn state => {\it tactic-valued expression}) 2.35 -\end{ttbox} 2.36 +\item[\ttindexbold{PRIMITIVE} $f$] packages the meta-rule~$f$ as a tactic that 2.37 + applies $f$ to the proof state and returns the result as a one-element 2.38 + sequence. If $f$ raises an exception, then the tactic's result is the empty 2.39 + sequence. 2.40 2.41 \item[\ttindexbold{SUBGOAL} $f$ $i$] 2.42 extracts subgoal~$i$ from the proof state as a term~$t$, and computes a

3.1 --- a/src/Pure/tctical.ML Wed Jul 23 11:11:14 1997 +0200 3.2 +++ b/src/Pure/tctical.ML Wed Jul 23 11:48:59 1997 +0200 3.3 @@ -49,7 +49,6 @@ 3.4 val REPEAT_SOME : (int -> tactic) -> tactic 3.5 val SELECT_GOAL : tactic -> int -> tactic 3.6 val SOMEGOAL : (int -> tactic) -> tactic 3.7 - val STATE : (thm -> tactic) -> tactic 3.8 val strip_context : term -> (string * typ) list * term list * term 3.9 val SUBGOAL : ((term*int) -> tactic) -> int -> tactic 3.10 val suppress_tracing : bool ref 3.11 @@ -75,9 +74,6 @@ 3.12 3.13 type tactic = thm -> thm Sequence.seq; 3.14 3.15 -(*Makes a tactic from one that uses the components of the state.*) 3.16 -fun STATE tacfun st = tacfun st st; 3.17 - 3.18 3.19 (*** LCF-style tacticals ***) 3.20