# HG changeset patch
# User wenzelm
# Date 1138894291 -3600
# Node ID 45c7327823396958892a6cc859e8d76dad41078e
# Parent  b1e2151574c15c711cc580530cc47440cf2b5a3e
'obtain': optional case name;

diff -r b1e2151574c1 -r 45c732782339 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Feb 02 16:31:30 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Feb 02 16:31:31 2006 +0100
@@ -107,14 +107,13 @@
 \end{matharray}
 
 \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
-
-\railalias{printlocale}{print\_locale}
-\railterm{printlocale}
+\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
+\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
 
 \begin{rail}
   'locale' ('(open)')? name ('=' localeexpr)?
   ;
-  printlocale '!'? localeexpr
+  'print\_locale' '!'? localeexpr
   ;
   localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
   ;
@@ -391,7 +390,7 @@
 corresponding parameters do \emph{not} occur in the conclusion.
 
 \begin{rail}
-  'obtain' (vars + 'and') 'where' (props + 'and')
+  'obtain' parname? (vars + 'and') 'where' (props + 'and')
   ;
   'guess' (vars + 'and')
   ;
@@ -426,6 +425,9 @@
 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
 where the result is treated as a genuine assumption.
 
+An alternative name to be used instead of ``$that$'' above may be
+given in parentheses.
+
 \medskip
 
 The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but