# HG changeset patch # User wenzelm # Date 1086799876 -7200 # Node ID b9cc12a91fd3bc188530af51c0c52f2a7443c856 # Parent d23f6b505e9a5f02da76663eb5276df208c120e8 updated/tuned identifier syntax; diff -r d23f6b505e9a -r b9cc12a91fd3 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Wed Jun 09 18:51:02 2004 +0200 +++ b/doc-src/IsarRef/syntax.tex Wed Jun 09 18:51:16 2004 +0200 @@ -81,26 +81,21 @@ string & = & \verb,", ~\dots~ \verb,", \\ verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex] - letter & = & sletter ~|~ xletter \\ + letter & = & latin ~|~ symletter \\ + latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\ - quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\ + quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\ sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$ \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\ & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~ \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\ symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots\\ -sletter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\ -xletter & = & {\tt \backslash<} ~ (sletter ~|~ dletter ~|~ gletter ~|~ cletter) ~ {\tt >}\\ -dletter & = & \verb,aa, ~|~ \dots ~|~ \verb,zz, ~|~ \verb,AA, ~|~ \dots ~|~ \verb,ZZ, \\ -bletter & = & {\tt bool} ~|~ {\tt complex} ~|~ {\tt nat} ~|~ {\tt rat} ~|~ {\tt real} ~|~ {\tt int}\\ -cletter & = & {\tt \hat{}\, isup} ~~|~~ {\tt \hat{}\, isub} -\end{matharray} -\begin{matharray}{rcl} -gletter & = & {\tt alpha} ~|~ {\tt beta} ~|~ {\tt gamma} ~|~ {\tt delta} ~|~ {\tt epsilon} ~|~ {\tt zeta} ~|~ {\tt eta} ~|\\ - & & {\tt theta} ~|~ {\tt iota} ~|~ {\tt kappa} ~|~ {\tt mu} ~|~ {\tt nu} ~|~ {\tt xi} ~|~ {\tt pi} ~|~ {\tt rho} ~|\\ - & & {\tt sigma} ~|~ {\tt tau} ~|~ {\tt upsilon} ~|~ {\tt phi} ~|~ {\tt psi} ~|~ {\tt omega} ~|~ {\tt Gamma} ~|\\ - & & {\tt Delta} ~|~ {\tt Theta} ~|~ {\tt Lambda} ~|~ {\tt Xi} ~|~ {\tt Pi} ~|~ {\tt Sigma} ~|~ {\tt Upsilon} ~|\\ - & & {\tt Phi} ~|~ {\tt Psi} ~|~ {\tt Omega} +symletter & = & \verb,\<, (latin ~|~ latin~latin ~|~ greek) \verb,>, \\ +greek & = & \verb,alpha, ~|~ \verb,beta, ~|~ \verb,gamma, ~|~ \verb,delta, ~|~ \verb,epsilon, ~|~ \verb,zeta, ~|~ \verb,eta, ~| \\ + & & \verb,theta, ~|~ \verb,iota, ~|~ \verb,kappa, ~|~ \verb,mu, ~|~ \verb,nu, ~|~ \verb,xi, ~|~ \verb,pi, ~|~ \verb,rho, ~| \\ + & & \verb,sigma, ~|~ \verb,tau, ~|~ \verb,upsilon, ~|~ \verb,phi, ~|~ \verb,psi, ~|~ \verb,omega, ~|~ \verb,Gamma, ~| \\ + & & \verb,Delta, ~|~ \verb,Theta, ~|~ \verb,Lambda, ~|~ \verb,Xi, ~|~ \verb,Pi, ~|~ \verb,Sigma, ~|~ \verb,Upsilon, ~| \\ + & & \verb,Phi, ~|~ \verb,Psi, ~|~ \verb,Omega, \end{matharray} The syntax of $string$ admits any characters, including newlines; ``\verb|"|'' @@ -128,11 +123,9 @@ Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as ``\verb,\,''. Concerning Isabelle itself, any sequence of the form \verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. -Greek letters \verb+\+, \verb+\+, etc (apart from -\verb+\+), caligraphic letters in various styles, as -well as the special \verb+\<^isub>+ and \verb+\<^isup>+ sub/superscipt -control characters are considered proper letters and can be used as -part of any identifier. +Greek letters \verb+\+, \verb+\+, etc. (apart from +\verb+\+), as well as the \verb+\<^isub>+ and \verb+\<^isup>+ control +characters may be used in identifiers as well. Display of appropriate glyphs is a matter of front-end tools, say the user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX} @@ -146,8 +139,8 @@ terms, and theorem specifications, which have been factored out of the actual Isar language elements to be described later. -Note that some of the basic syntactic entities introduced below (e.g.\ -\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\ +Note that some of the basic syntactic entities introduced below (e.g.\ +\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\ \railnonterm{sort}), especially for the sake of error messages. E.g.\ syntax elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would really report a missing name or type rather than any of the constituent @@ -159,7 +152,7 @@ Entity \railqtok{name} usually refers to any name of types, constants, theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified identifiers are excluded here). Quoted strings provide an escape for -non-identifier names or those ruled out by outer syntax keywords (e.g.\ +non-identifier names or those ruled out by outer syntax keywords (e.g.\ \verb|"let"|). Already existing objects are usually referenced by \railqtok{nameref}. @@ -471,7 +464,7 @@ \texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|. \begin{descr} - + \item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute specifications may be included as well (see also \S\ref{sec:syn-att}); the $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly @@ -482,12 +475,12 @@ \item [$\at\{term~t\}$] prints a well-typed term $t$. \item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$. - + \item [$\at\{text~s\}$] prints uninterpreted source text $s$. This is particularly useful to print portions of text according to the Isabelle {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces of terms that should not be parsed or type-checked yet). - + \item [$\at\{goals\}$] prints the current \emph{dynamic} goal state. This is mainly for support of tactic-emulation scripts within Isar --- presentation of goal states does not conform to actual human-readable proof documents. @@ -538,6 +531,9 @@ admits arbitrary output). \item[$goals_limit = nat$] determines the maximum number of goals to be printed. +\item[$locale = name$] specifies an alternative context used for evaluating + and printing the subsequent argument. Note that a proof context is escaped + to the enclosing theory context first. \end{descr} For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''. All of @@ -549,7 +545,7 @@ well-formedness of terms and types with respect to the current theory or proof context is ensured here. -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: "isar-ref" -%%% End: +%%% End: