'iff' attribute;
authorwenzelm
Mon Aug 30 14:11:47 1999 +0200 (1999-08-30)
changeset 7391b7ca64c8fa64
parent 7390 f819265e267c
child 7392 4137c951b36b
'iff' attribute;
doc-src/IsarRef/generic.tex
     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.