doc-src/IsarRef/generic.tex
 changeset 7391 b7ca64c8fa64 parent 7356 1714c91b8729 child 7396 d3f231fe725c
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 30 14:08:37 1999 +0200
1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 30 14:11:47 1999 +0200
1.3 @@ -138,7 +138,7 @@
1.4
1.5  Calculational proof is forward reasoning with implicit application of
1.6  transitivity rules (such those of $=$, $\le$, $<$).  Isabelle/Isar maintains
1.7 -an auxiliary register $calculation$\indexisarreg{calculation} for accumulating
1.8 +an auxiliary register $calculation$\indexisarthm{calculation} for accumulating
1.9  results obtained by transitivity obtained together with the current facts.
1.10  Command $\ALSO$ updates $calculation$ from the most recent result, while
1.11  $\FINALLY$ exhibits the final result by forward chaining towards the next goal
1.12 @@ -243,7 +243,7 @@
1.13
1.14  \subsection{Simplification methods}\label{sec:simp}
1.15
1.16 -\indexisarmeth{simp}\indexisarmeth{asm_simp}
1.17 +\indexisarmeth{simp}\indexisarmeth{asm-simp}
1.18  \begin{matharray}{rcl}
1.19    simp & : & \isarmeth \\
1.20    asm_simp & : & \isarmeth \\
1.21 @@ -294,7 +294,8 @@
1.22
1.23  \subsection{Forward simplification}
1.24
1.25 -\indexisaratt{simplify}\indexisaratt{asm_simplify}\indexisaratt{full_simplify}\indexisaratt{asm_full_simplify}
1.26 +\indexisaratt{simplify}\indexisaratt{asm-simplify}
1.27 +\indexisaratt{full-simplify}\indexisaratt{asm-full-simplify}
1.28  \begin{matharray}{rcl}
1.29    simplify & : & \isaratt \\
1.30    asm_simplify & : & \isaratt \\
1.31 @@ -348,7 +349,7 @@
1.32  \subsection{Automatic methods}\label{sec:classical-auto}
1.33
1.34  \indexisarmeth{blast}
1.35 -\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow_best}
1.36 +\indexisarmeth{fast}\indexisarmeth{best}\indexisarmeth{slow}\indexisarmeth{slow-best}
1.37  \begin{matharray}{rcl}
1.38   blast & : & \isarmeth \\
1.39   fast & : & \isarmeth \\
1.40 @@ -410,11 +411,13 @@
1.41
1.42  \subsection{Modifying the context}\label{sec:classical-mod}
1.43
1.44 -\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{delrule}
1.45 +\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
1.46 +\indexisaratt{iff}\indexisaratt{delrule}
1.47  \begin{matharray}{rcl}
1.48    intro & : & \isaratt \\
1.49    elim & : & \isaratt \\
1.50    dest & : & \isaratt \\
1.51 +  iff & : & \isaratt \\
1.52    delrule & : & \isaratt \\
1.53  \end{matharray}
1.54
1.55 @@ -429,6 +432,9 @@
1.56    single !'' classifies as \emph{unsafe}, and !!'' as \emph{extra} (i.e.\
1.57    not applied in the search-oriented automatic methods).
1.58
1.59 +\item [$iff$] declares equations both as rewrite rules for the simplifier and
1.60 +  classical reasoning rules.
1.61 +
1.62  \item [$delrule$] deletes introduction or elimination rules from the context.
1.63    Note that destruction rules would have to be turned into elimination rules
1.64    first, e.g.\ by using the $elimify$ attribute.