# 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}