# HG changeset patch
# User wenzelm
# Date 955640948 -7200
# Node ID d90bab9d001b7cf46d5a1fac243060505319a933
# Parent  483a3eb96c7e5650a53a5a1c63c7d720f8e1e29d
recdef: no simps;

diff -r 483a3eb96c7e -r d90bab9d001b doc-src/IsarRef/hol.tex
--- 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}