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