doc-src/IsarRef/generic.tex
changeset 9703 bf65780eed02
parent 9642 d8d1f70024bd
child 9711 75df6a20b0b3
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:19 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 28 20:29:56 2000 +0200
     1.3 @@ -620,16 +620,19 @@
     1.4  
     1.5  \section{Basic equational reasoning}
     1.6  
     1.7 -\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisaratt{symmetric}
     1.8 +\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
     1.9  \begin{matharray}{rcl}
    1.10    subst & : & \isarmeth \\
    1.11    hypsubst^* & : & \isarmeth \\
    1.12 +  split & : & \isarmeth \\
    1.13    symmetric & : & \isaratt \\
    1.14  \end{matharray}
    1.15  
    1.16  \begin{rail}
    1.17    'subst' thmref
    1.18    ;
    1.19 +  'split' thmrefs
    1.20 +  ;
    1.21  \end{rail}
    1.22  
    1.23  These methods and attributes provide basic facilities for equational reasoning
    1.24 @@ -642,6 +645,9 @@
    1.25  \item [$subst~thm$] performs a single substitution step using rule $thm$,
    1.26    which may be either a meta or object equality.
    1.27  \item [$hypsubst$] performs substitution using some assumption.
    1.28 +\item [$split~thms$] performs single-step case splitting using rules $thms$.
    1.29 +  Note that the $simp$ method already involves repeated application of split
    1.30 +  rules as declared in the current context (see \S\ref{sec:simp}).
    1.31  \item [$symmetric$] applies the symmetry rule of meta or object equality.
    1.32  \end{descr}
    1.33