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 * ) ;