# HG changeset patch
# User wenzelm
# Date 1113053762 -7200
# Node ID 8fa8872cdc49e8d710fe8ff654fb9a2da152df01
# Parent  406a98ee802750de95a1f9707fe03411009ed383
thmref: selection syntax;

diff -r 406a98ee8027 -r 8fa8872cdc49 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Apr 09 15:35:37 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Apr 09 15:36:02 2005 +0200
@@ -338,14 +338,17 @@
 \railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
 statements, while \railnonterm{thmdef} collects lists of existing theorems.
 Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
-the former requires an actual singleton result.  Any of these theorem
-specifications may include lists of attributes both on the left and right hand
-sides; attributes are applied to any immediately preceding fact.  If names are
-omitted, the theorems are not stored within the theorem database of the theory
-or proof context; any given attributes are still applied, though.
+the former requires an actual singleton result.  An optional index selection
+specifies the individual theorems to be picked out of a given fact list.  Any
+kind of theorem specification may include lists of attributes both on the left
+and right hand sides; attributes are applied to any immediately preceding
+fact.  If names are omitted, the theorems are not stored within the theorem
+database of the theory or proof context, but any given attributes are applied
+nonetheless.
 
-\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
-\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
+\indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
+\indexouternonterm{thmdef}\indexouternonterm{thmref}
+\indexouternonterm{thmrefs}\indexouternonterm{selection}
 \begin{rail}
   axmdecl: name attributes? ':'
   ;
@@ -353,13 +356,15 @@
   ;
   thmdef: thmbind '='
   ;
-  thmref: nameref attributes?
+  thmref: nameref selection? attributes?
   ;
   thmrefs: thmref +
   ;
 
   thmbind: name attributes | name | attributes
   ;
+  selection: '(' ((nat | nat '-' nat?) + ',') ')'
+  ;
 \end{rail}