added 'cong' att;
authorwenzelm
Fri Mar 31 21:57:14 2000 +0200 (2000-03-31)
changeset 863821cb46716f32
parent 8637 e86e49aa1631
child 8639 31bcb6b64d60
added 'cong' att;
fixed 'iff' syntax;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Fri Mar 31 21:56:23 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Mar 31 21:57:14 2000 +0200
     1.3 @@ -417,20 +417,22 @@
     1.4  
     1.5  \subsection{Declaring rules}
     1.6  
     1.7 -\indexisaratt{simp}\indexisaratt{split}
     1.8 +\indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong}
     1.9  \begin{matharray}{rcl}
    1.10    simp & : & \isaratt \\
    1.11    split & : & \isaratt \\
    1.12 +  cong & : & \isaratt \\
    1.13  \end{matharray}
    1.14  
    1.15  \begin{rail}
    1.16 -  ('simp' | 'split') (() | 'add' | 'del')
    1.17 +  ('simp' | 'split' | 'cong') (() | 'add' | 'del')
    1.18    ;
    1.19  \end{rail}
    1.20  
    1.21  \begin{descr}
    1.22  \item [$simp$] declares simplification rules.
    1.23  \item [$split$] declares split rules.
    1.24 +\item [$cong$] declares congruence rules.
    1.25  \end{descr}
    1.26  
    1.27  
    1.28 @@ -583,6 +585,7 @@
    1.29  \begin{rail}
    1.30    ('intro' | 'elim' | 'dest') (() | '?' | '??')
    1.31    ;
    1.32 +  'iff' (() | 'add' | 'del')
    1.33  \end{rail}
    1.34  
    1.35  \begin{descr}