# HG changeset patch
# User wenzelm
# Date 1146955490 -7200
# Node ID a14871b57387582dc6b31681b294bebf23b90de2
# Parent  70a1ce3b23aeeda0c248e1313e662b2effb5c50c
removed 'concl is' pattern;

diff -r 70a1ce3b23ae -r a14871b57387 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sun May 07 00:22:05 2006 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sun May 07 00:44:50 2006 +0200
@@ -399,7 +399,7 @@
 \begin{rail}
   termpat: '(' ('is' term +) ')'
   ;
-  proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
+  proppat: '(' ('is' prop +) ')'
   ;
 \end{rail}