Removal of tactical STATE
authorpaulson
Wed Jul 23 11:48:59 1997 +0200 (1997-07-23)
changeset 3561329441e7eeee
parent 3560 7db9a44dfa06
child 3562 5380acac8c83
Removal of tactical STATE
NEWS
doc-src/Ref/tactic.tex
src/Pure/tctical.ML
     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