doc-src/IsarRef/pure.tex
changeset 8632 14a69a0e8679
parent 8620 3786d47f5570
child 8664 aa383eeb3359
--- a/doc-src/IsarRef/pure.tex	Fri Mar 31 10:23:15 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Mar 31 18:10:21 2000 +0200
@@ -630,7 +630,7 @@
   ('have' | 'show' | 'hence' | 'thus') goal
   ;
 
-  goal: thmdecl? proppat comment?
+  goal: thmdecl? prop proppat? comment?
   ;
 \end{rail}