# HG changeset patch
# User wenzelm
# Date 954519021 -7200
# Node ID 14a69a0e86792e4740622e27ac185937183b3f65
# Parent  a10ae360b63c0b1c3f5800608994de6fb0ccf1a0
fixed goal syntax;

diff -r a10ae360b63c -r 14a69a0e8679 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}