--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 22:05:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 22:05:49 2006 +0200
@@ -692,7 +692,7 @@
\begin{itemize}
- \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
+ \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},
\item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
@@ -750,32 +750,26 @@
name components. The packed representation a dot as separator, for
example in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called
\emph{base} name, the remaining prefix \emph{qualifier} (which may
- be empty).
+ be empty). The basic idea of qualified names is to encode a
+ hierarchically structured name spaces by recording the access path
+ as part of the name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood
+ as a local entity \isa{c} within a local structure \isa{b}
+ of the enclosing structure \isa{A}. Typically, name space
+ hierarchies consist of 1--3 levels, but this need not be always so.
The empty name is commonly used as an indication of unnamed
entities, if this makes any sense. The operations on qualified
names are smart enough to pass through such improper names
unchanged.
- The basic idea of qualified names is to encode a hierarchically
- structured name spaces by recording the access path as part of the
- name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
- entity \isa{c} within a local structure \isa{b} of the
- enclosing structure \isa{A}. Typically, name space hierarchies
- consist of 1--3 levels, but this need not be always so.
-
\medskip A \isa{naming} policy tells how to turn a name
specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
- externally.
-
- For example, the default naming prefixes an implicit path from the
- context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
- standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
- partial \isa{path} specifications.
-
+ externally. For example, the default naming prefixes an implicit
+ path from the context: \isa{x} is becomes \isa{path{\isachardot}x}
+ internally; the standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further partial \isa{path} specifications.
Normally, the naming is implicit in the theory or proof context.
- There are separate versions of the corresponding operations for these
- context types.
+ There are separate versions of the corresponding operations for
+ these context types.
\medskip A \isa{name\ space} manages a collection of fully
internalized names, together with a mapping between external names
@@ -787,19 +781,18 @@
of formal entity, such as logical constant, type, type class,
theorem etc. It is usually clear from the occurrence in concrete
syntax (or from the scope) which kind of entity a name refers to.
-
For example, the very same name \isa{c} may be used uniformly
for a constant, type, type class, which are from separate syntactic
- categories. There is a common convention to name theorems
- systematically, according to the name of the main logical entity
- being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
- theorems related to constant \isa{c}.
+ categories.
- This technique of mapping names from one space into another requires
- some care in order to avoid conflicts. In particular, theorem names
- derived from type or class names are better suffixed in addition to
- the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
- \isa{c}, respectively.%
+ There are common schemes to name theorems systematically, according
+ to the name of the main logical entity being involved, such as
+ \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for theorems related to
+ constant \isa{c}. This technique of mapping names from one
+ space into another requires some care in order to avoid conflicts.
+ In particular, theorem names derived from type or class names are
+ better suffixed in addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to
+ type \isa{c} and class \isa{c}, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
%