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