author wenzelm Tue Sep 05 22:05:15 2006 +0200 (2006-09-05) changeset 20479 1e496953ed7d parent 20478 de1bd9717d6c child 20480 4e0522d38968
tuned;
     1.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Tue Sep 05 22:04:56 2006 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Tue Sep 05 22:05:15 2006 +0200
1.3 @@ -601,7 +601,7 @@
1.4
1.5    \begin{itemize}
1.6
1.7 -  \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"}.
1.8 +  \item @{text "?x"} if @{text "x"} does not end with a digit and @{text "i = 0"},
1.9
1.10    \item @{text "?xi"} if @{text "x"} does not end with a digit,
1.11
1.12 @@ -644,33 +644,28 @@
1.13    name components.  The packed representation a dot as separator, for
1.14    example in @{text "A.b.c"}''.  The last component is called
1.15    \emph{base} name, the remaining prefix \emph{qualifier} (which may
1.16 -  be empty).
1.17 +  be empty).  The basic idea of qualified names is to encode a
1.18 +  hierarchically structured name spaces by recording the access path
1.19 +  as part of the name.  For example, @{text "A.b.c"} may be understood
1.20 +  as a local entity @{text "c"} within a local structure @{text "b"}
1.21 +  of the enclosing structure @{text "A"}.  Typically, name space
1.22 +  hierarchies consist of 1--3 levels, but this need not be always so.
1.23
1.24    The empty name is commonly used as an indication of unnamed
1.25    entities, if this makes any sense.  The operations on qualified
1.26    names are smart enough to pass through such improper names
1.27    unchanged.
1.28
1.29 -  The basic idea of qualified names is to encode a hierarchically
1.30 -  structured name spaces by recording the access path as part of the
1.31 -  name.  For example, @{text "A.b.c"} may be understood as a local
1.32 -  entity @{text "c"} within a local structure @{text "b"} of the
1.33 -  enclosing structure @{text "A"}.  Typically, name space hierarchies
1.34 -  consist of 1--3 levels, but this need not be always so.
1.35 -
1.36    \medskip A @{text "naming"} policy tells how to turn a name
1.37    specification into a fully qualified internal name (by the @{text
1.38    "full"} operation), and how to fully qualified names may be accessed
1.39 -  externally.
1.40 -
1.41 -  For example, the default naming prefixes an implicit path from the
1.42 -  context: @{text "x"} is becomes @{text "path.x"} internally; the
1.43 -  standard accesses include @{text "x"}, @{text "path.x"}, and further
1.44 -  partial @{text "path"} specifications.
1.45 -
1.46 +  externally.  For example, the default naming prefixes an implicit
1.47 +  path from the context: @{text "x"} is becomes @{text "path.x"}
1.48 +  internally; the standard accesses include @{text "x"}, @{text
1.49 +  "path.x"}, and further partial @{text "path"} specifications.
1.50    Normally, the naming is implicit in the theory or proof context.
1.51 -  There are separate versions of the corresponding operations for these
1.52 -  context types.
1.53 +  There are separate versions of the corresponding operations for
1.54 +  these context types.
1.55
1.56    \medskip A @{text "name space"} manages a collection of fully
1.57    internalized names, together with a mapping between external names
1.58 @@ -683,20 +678,19 @@
1.59    of formal entity, such as logical constant, type, type class,
1.60    theorem etc.  It is usually clear from the occurrence in concrete
1.61    syntax (or from the scope) which kind of entity a name refers to.
1.62 -
1.63    For example, the very same name @{text "c"} may be used uniformly
1.64    for a constant, type, type class, which are from separate syntactic
1.65 -  categories.  There is a common convention to name theorems
1.66 -  systematically, according to the name of the main logical entity
1.67 -  being involved, such as @{text "c.intro"} and @{text "c.elim"} for
1.68 -  theorems related to constant @{text "c"}.
1.69 +  categories.
1.70
1.71 -  This technique of mapping names from one space into another requires
1.72 -  some care in order to avoid conflicts.  In particular, theorem names
1.73 -  derived from type or class names are better suffixed in addition to
1.74 -  the usual qualification, e.g.\ @{text "c_type.intro"} and @{text
1.75 -  "c_class.intro"} for theorems related to type @{text "c"} and class
1.76 -  @{text "c"}, respectively.
1.77 +  There are common schemes to name theorems systematically, according
1.78 +  to the name of the main logical entity being involved, such as
1.79 +  @{text "c.intro"} and @{text "c.elim"} for theorems related to
1.80 +  constant @{text "c"}.  This technique of mapping names from one
1.81 +  space into another requires some care in order to avoid conflicts.
1.82 +  In particular, theorem names derived from type or class names are
1.83 +  better suffixed in addition to the usual qualification, e.g.\ @{text
1.84 +  "c_type.intro"} and @{text "c_class.intro"} for theorems related to
1.85 +  type @{text "c"} and class @{text "c"}, respectively.
1.86  *}
1.87
1.88  text %mlref {*