--- a/doc-src/IsarRef/generic.tex Fri Mar 31 21:56:23 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Fri Mar 31 21:57:14 2000 +0200
@@ -417,20 +417,22 @@
\subsection{Declaring rules}
-\indexisaratt{simp}\indexisaratt{split}
+\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
\begin{matharray}{rcl}
simp & : & \isaratt \\
split & : & \isaratt \\
+ cong & : & \isaratt \\
\end{matharray}
\begin{rail}
- ('simp' | 'split') (() | 'add' | 'del')
+ ('simp' | 'split' | 'cong') (() | 'add' | 'del')
;
\end{rail}
\begin{descr}
\item [$simp$] declares simplification rules.
\item [$split$] declares split rules.
+\item [$cong$] declares congruence rules.
\end{descr}
@@ -583,6 +585,7 @@
\begin{rail}
('intro' | 'elim' | 'dest') (() | '?' | '??')
;
+ 'iff' (() | 'add' | 'del')
\end{rail}
\begin{descr}