--- a/doc-src/IsarRef/hol.tex Thu Apr 13 15:19:37 2000 +0200
+++ b/doc-src/IsarRef/hol.tex Thu Apr 13 17:49:08 2000 +0200
@@ -136,7 +136,7 @@
equation: thmdecl? prop comment?
;
- hints: ('congs' thmrefs)? ('simpset' name)?
+ hints: ('congs' thmrefs)?
;
\end{rail}