# HG changeset patch
# User wenzelm
# Date 982194825 -3600
# Node ID 48c63b87566e1a65364c7982f4c94e356a5193b3
# Parent  e43723fff70c4d5d1d11876cbfe90e3234696202
index mod syntax;

diff -r e43723fff70c -r 48c63b87566e doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Feb 14 23:43:55 2001 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Feb 15 00:53:45 2001 +0100
@@ -531,6 +531,7 @@
 \railalias{noasmuse}{no\_asm\_use}
 \railterm{noasmuse}
 
+\indexouternonterm{simpmod}
 \begin{rail}
   ('simp' | simpall) ('!' ?) opt? (simpmod * )
   ;
@@ -728,6 +729,7 @@
   clarify & : & \isarmeth \\
 \end{matharray}
 
+\indexouternonterm{clamod}
 \begin{rail}
   'blast' ('!' ?) nat? (clamod * )
   ;
@@ -771,6 +773,7 @@
   bestsimp & : & \isarmeth \\
 \end{matharray}
 
+\indexouternonterm{clasimpmod}
 \begin{rail}
   'auto' '!'? (nat nat)? (clasimpmod * )
   ;