# HG changeset patch
# User wenzelm
# Date 954532634 -7200
# Node ID 21cb46716f32e214494a6253a421edd31ed615ca
# Parent  e86e49aa1631f5f702871d9e29b3fa4354e9b14a
added 'cong' att;
fixed 'iff' syntax;

diff -r e86e49aa1631 -r 21cb46716f32 doc-src/IsarRef/generic.tex
--- 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}