doc-src/IsarRef/generic.tex
changeset 7990 0a604b2fc2b1
parent 7987 d9aef93c0e32
child 8195 af2575a5c5ae
     1.1 --- a/doc-src/IsarRef/generic.tex	Sun Oct 31 15:26:37 1999 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Sun Oct 31 20:11:23 1999 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4  \indexisaratt{tag}\indexisaratt{untag}\indexisaratt{COMP}\indexisaratt{RS}
     1.5  \indexisaratt{OF}\indexisaratt{where}\indexisaratt{of}\indexisaratt{standard}
     1.6  \indexisaratt{elimify}\indexisaratt{transfer}\indexisaratt{export}
     1.7 +\indexisaratt{unfold}\indexisaratt{fold}
     1.8  \begin{matharray}{rcl}
     1.9    tag & : & \isaratt \\
    1.10    untag & : & \isaratt \\[0.5ex]
    1.11 @@ -69,10 +70,12 @@
    1.12    COMP & : & \isaratt \\[0.5ex]
    1.13    of & : & \isaratt \\
    1.14    where & : & \isaratt \\[0.5ex]
    1.15 +  unfold & : & \isaratt \\
    1.16 +  fold & : & \isaratt \\[0.5ex]
    1.17    standard & : & \isaratt \\
    1.18    elimify & : & \isaratt \\
    1.19    export^* & : & \isaratt \\
    1.20 -  transfer & : & \isaratt \\
    1.21 +  transfer & : & \isaratt \\[0.5ex]
    1.22  \end{matharray}
    1.23  
    1.24  \begin{rail}
    1.25 @@ -86,6 +89,8 @@
    1.26    ;
    1.27    'where' (name '=' term * 'and')
    1.28    ;
    1.29 +  ('unfold' | 'fold') thmrefs
    1.30 +  ;
    1.31  
    1.32    inst: underscore | term
    1.33    ;
    1.34 @@ -108,7 +113,12 @@
    1.35  \item [$of~\vec t$ and $where~\vec x = \vec t$] perform positional and named
    1.36    instantiation, respectively.  The terms given in $of$ are substituted for
    1.37    any schematic variables occurring in a theorem from left to right;
    1.38 -  ``\texttt{_}'' (underscore) indicates to skip a position.
    1.39 +  ``\texttt{_}'' (underscore) indicates to skip a position.  Arguments
    1.40 +  following a ``$concl\colon$'' specification refer to positions of the
    1.41 +  conclusion of a rule.
    1.42 +  
    1.43 +\item [$unfold~thms$ and $fold~thms$] expand and fold back again the given
    1.44 +  meta-level definitions throughout a rule.
    1.45   
    1.46  \item [$standard$] puts a theorem into the standard form of object-rules, just
    1.47    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
    1.48 @@ -447,7 +457,8 @@
    1.49  \item [$intro$, $elim$, $dest$] add introduction, elimination, destruct rules,
    1.50    respectively.  By default, rules are considered as \emph{safe}, while a
    1.51    single ``!'' classifies as \emph{unsafe}, and ``!!'' as \emph{extra} (i.e.\ 
    1.52 -  not applied in the search-oriented automated methods, but only $rule$).
    1.53 +  not applied in the search-oriented automated methods, but only in
    1.54 +  single-step methods such as $rule$).
    1.55    
    1.56  \item [$iff$] declares equations both as rewrite rules for the simplifier and
    1.57    classical reasoning rules.