fixed goal syntax;
authorwenzelm
Fri, 31 Mar 2000 18:10:21 +0200
changeset 8632 14a69a0e8679
parent 8631 a10ae360b63c
child 8633 427ead639d8a
fixed goal syntax;
doc-src/IsarRef/pure.tex
--- 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}