tuned;
authorwenzelm
Thu Sep 07 15:16:26 2006 +0200 (2006-09-07)
changeset 20488121bc2135bd3
parent 20487 6ac7a4fc32a0
child 20489 a684fc70d04e
tuned;
doc-src/IsarImplementation/Thy/prelim.thy
doc-src/IsarImplementation/implementation.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Sep 06 22:48:36 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Thu Sep 07 15:16:26 2006 +0200
     1.3 @@ -137,8 +137,8 @@
     1.4  
     1.5    \medskip There is a separate notion of \emph{theory reference} for
     1.6    maintaining a live link to an evolving theory context: updates on
     1.7 -  drafts are propagated automatically.  The dynamic stops after an
     1.8 -  explicit @{text "end"} only.
     1.9 +  drafts are propagated automatically.  Dynamic updating stops after
    1.10 +  an explicit @{text "end"} only.
    1.11  
    1.12    Derived entities may store a theory reference in order to indicate
    1.13    the context they belong to.  This implicitly assumes monotonic
    1.14 @@ -408,12 +408,11 @@
    1.15  
    1.16  text {*
    1.17    In principle, a name is just a string, but there are various
    1.18 -  convention for encoding additional structure.
    1.19 -
    1.20 -  For example, the string ``@{text "Foo.bar.baz"}'' is considered as a
    1.21 -  qualified name.  The most basic constituents of names may have their
    1.22 -  own structure, e.g.\ the string ``\verb,\,\verb,<alpha>,'' is
    1.23 -  considered as a single symbol (printed as ``@{text "\<alpha>"}'').
    1.24 +  convention for encoding additional structure.  For example, ``@{text
    1.25 +  "Foo.bar.baz"}'' is considered as a qualified name consisting of
    1.26 +  three basic name components.  The individual constituents of a name
    1.27 +  may have further substructure, e.g.\ the string
    1.28 +  ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.
    1.29  *}
    1.30  
    1.31  
    1.32 @@ -425,28 +424,28 @@
    1.33    symbols (for greek, math etc.).}
    1.34  
    1.35    A \emph{symbol} constitutes the smallest textual unit in Isabelle
    1.36 -  --- raw characters are normally not encountered.  Isabelle strings
    1.37 -  consist of a sequence of symbols, represented as a packed string or
    1.38 -  a list of symbols.  Each symbol is in itself a small string, which
    1.39 -  is of one of the following forms:
    1.40 +  --- raw characters are normally not encountered at all.  Isabelle
    1.41 +  strings consist of a sequence of symbols, represented as a packed
    1.42 +  string or a list of strings.  Each symbol is in itself a small
    1.43 +  string, which has either one of the following forms:
    1.44  
    1.45    \begin{enumerate}
    1.46  
    1.47 -  \item singleton ASCII character ``@{text "c"}'' (character code
    1.48 -  0--127), for example ``\verb,a,'',
    1.49 +  \item a single ASCII character ``@{text "c"}'', for example
    1.50 +  ``\verb,a,'',
    1.51  
    1.52 -  \item regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
    1.53 +  \item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
    1.54    for example ``\verb,\,\verb,<alpha>,'',
    1.55  
    1.56 -  \item control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'',
    1.57 +  \item a control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'',
    1.58    for example ``\verb,\,\verb,<^bold>,'',
    1.59  
    1.60 -  \item raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,'' where
    1.61 -  @{text text} is constists of printable characters excluding
    1.62 +  \item a raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,''
    1.63 +  where @{text text} constists of printable characters excluding
    1.64    ``\verb,.,'' and ``\verb,>,'', for example
    1.65    ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
    1.66  
    1.67 -  \item numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
    1.68 +  \item a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
    1.69    n}\verb,>, where @{text n} consists of digits, for example
    1.70    ``\verb,\,\verb,<^raw42>,''.
    1.71  
    1.72 @@ -457,15 +456,14 @@
    1.73    A..Za..z"} and @{text "digit = 0..9"}.  There are infinitely many
    1.74    regular symbols and control symbols, but a fixed collection of
    1.75    standard symbols is treated specifically.  For example,
    1.76 -  ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
    1.77 -  which means it may occur within regular Isabelle identifier syntax.
    1.78 +  ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
    1.79 +  may occur within regular Isabelle identifiers.
    1.80  
    1.81 -  Note that the character set underlying Isabelle symbols is plain
    1.82 -  7-bit ASCII.  Since 8-bit characters are passed through
    1.83 -  transparently, Isabelle may process Unicode/UCS data (in UTF-8
    1.84 -  encoding) as well.  Unicode provides its own collection of
    1.85 -  mathematical symbols, but there is no built-in link to the ones of
    1.86 -  Isabelle.
    1.87 +  Since the character set underlying Isabelle symbols is 7-bit ASCII
    1.88 +  and 8-bit characters are passed through transparently, Isabelle may
    1.89 +  also process Unicode/UCS data in UTF-8 encoding.  Unicode provides
    1.90 +  its own collection of mathematical symbols, but there is no built-in
    1.91 +  link to the standard collection of Isabelle.
    1.92  
    1.93    \medskip Output of Isabelle symbols depends on the print mode
    1.94    (\secref{FIXME}).  For example, the standard {\LaTeX} setup of the
    1.95 @@ -489,12 +487,11 @@
    1.96  
    1.97    \begin{description}
    1.98  
    1.99 -  \item @{ML_type "Symbol.symbol"} represents Isabelle symbols.  This
   1.100 -  type is an alias for @{ML_type "string"}, but emphasizes the
   1.101 -  specific format encountered here.
   1.102 +  \item @{ML_type "Symbol.symbol"} represents individual Isabelle
   1.103 +  symbols; this is an alias for @{ML_type "string"}.
   1.104  
   1.105    \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
   1.106 -  from the packed form that.  This function supercedes @{ML
   1.107 +  from the packed form.  This function supercedes @{ML
   1.108    "String.explode"} for virtually all purposes of manipulating text in
   1.109    Isabelle!
   1.110  
   1.111 @@ -504,8 +501,8 @@
   1.112    \cite{isabelle-isar-ref}.
   1.113  
   1.114    \item @{ML_type "Symbol.sym"} is a concrete datatype that represents
   1.115 -  the different kinds of symbols explicitly with constructors @{ML
   1.116 -  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML
   1.117 +  the different kinds of symbols explicitly, with constructors @{ML
   1.118 +  "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML
   1.119    "Symbol.Raw"}.
   1.120  
   1.121    \item @{ML "Symbol.decode"} converts the string representation of a
   1.122 @@ -529,27 +526,27 @@
   1.123    @{text "foo_"}, with Skolem versions @{text "foo__"} and @{text
   1.124    "foo___"}, respectively.
   1.125  
   1.126 -  Such special versions are required for bookkeeping of names that are
   1.127 -  apart from anything that may appear in the text given by the user.
   1.128 -  In particular, system generated variables in high-level Isar proof
   1.129 -  contexts are usually marked as internal, which prevents mysterious
   1.130 -  name references such as @{text "xaa"} in the text.
   1.131 +  These special versions provide copies of the basic name space, apart
   1.132 +  from anything that normally appears in the user text.  For example,
   1.133 +  system generated variables in Isar proof contexts are usually marked
   1.134 +  as internal, which prevents mysterious name references like @{text
   1.135 +  "xaa"} to appear in the text.
   1.136  
   1.137 -  \medskip Basic manipulations of binding scopes requires names to be
   1.138 -  modified.  A \emph{name context} contains a collection of already
   1.139 -  used names, which is maintained by the @{text "declare"} operation.
   1.140 +  \medskip Manipulating binding scopes often requires on-the-fly
   1.141 +  renamings.  A \emph{name context} contains a collection of already
   1.142 +  used names.  The @{text "declare"} operation adds names to the
   1.143 +  context.
   1.144  
   1.145 -  The @{text "invents"} operation derives a number of fresh names
   1.146 -  derived from a given starting point.  For example, three names
   1.147 -  derived from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"},
   1.148 -  provided there are no clashes with already used names.
   1.149 +  The @{text "invents"} operation derives a number of fresh names from
   1.150 +  a given starting point.  For example, the first three names derived
   1.151 +  from @{text "a"} are @{text "a"}, @{text "b"}, @{text "c"}.
   1.152  
   1.153    The @{text "variants"} operation produces fresh names by
   1.154 -  incrementing given names as to base-26 numbers (with digits @{text
   1.155 -  "a..z"}).  For example, name @{text "foo"} results in variants
   1.156 -  @{text "fooa"}, @{text "foob"}, @{text "fooc"}, \dots, @{text
   1.157 -  "fooaa"}, @{text "fooab"}, \dots; each renaming step picks the next
   1.158 -  unused variant from this list.
   1.159 +  incrementing tentative names as base-26 numbers (with digits @{text
   1.160 +  "a..z"}) until all clashes are resolved.  For example, name @{text
   1.161 +  "foo"} results in variants @{text "fooa"}, @{text "foob"}, @{text
   1.162 +  "fooc"}, \dots, @{text "fooaa"}, @{text "fooab"} etc.; each renaming
   1.163 +  step picks the next unused variant from this sequence.
   1.164  *}
   1.165  
   1.166  text %mlref {*
   1.167 @@ -574,11 +571,14 @@
   1.168    \item @{ML_type Name.context} represents the context of already used
   1.169    names; the initial value is @{ML "Name.context"}.
   1.170  
   1.171 -  \item @{ML Name.declare}~@{text "name"} declares @{text "name"} as
   1.172 -  being used.
   1.173 +  \item @{ML Name.declare}~@{text "name"} enters a used name into the
   1.174 +  context.
   1.175  
   1.176 -  \item @{ML Name.invents}~@{text "context base n"} produces @{text
   1.177 -  "n"} fresh names derived from @{text "base"}.
   1.178 +  \item @{ML Name.invents}~@{text "context name n"} produces @{text
   1.179 +  "n"} fresh names derived from @{text "name"}.
   1.180 +
   1.181 +  \item @{ML Name.variants}~@{text "names context"} produces fresh
   1.182 +  varians of @{text "names"}; the result is entered into the context.
   1.183  
   1.184    \end{description}
   1.185  *}
   1.186 @@ -588,16 +588,20 @@
   1.187  
   1.188  text {*
   1.189    An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic
   1.190 -  name with a natural number.  This representation allows efficient
   1.191 -  renaming by incrementing the second component only.  To rename two
   1.192 -  collections of indexnames apart from each other, first determine the
   1.193 -  maximum index @{text "maxidx"} of the first collection, then
   1.194 -  increment all indexes of the second collection by @{text "maxidx +
   1.195 -  1"}.  Note that the maximum index of an empty collection is @{text
   1.196 -  "-1"}.
   1.197 +  name and a natural number.  This representation allows efficient
   1.198 +  renaming by incrementing the second component only.  The canonical
   1.199 +  way to rename two collections of indexnames apart from each other is
   1.200 +  this: determine the maximum index @{text "maxidx"} of the first
   1.201 +  collection, then increment all indexes of the second collection by
   1.202 +  @{text "maxidx + 1"}; the maximum index of an empty collection is
   1.203 +  @{text "-1"}.
   1.204  
   1.205 -  Isabelle syntax observes the following rules for representing an
   1.206 -  indexname @{text "(x, i)"} as a packed string:
   1.207 +  Occasionally, basic names and indexed names are injected into the
   1.208 +  same pair type: the (improper) indexname @{text "(x, -1)"} is used
   1.209 +  to encode basic names.
   1.210 +
   1.211 +  \medskip Isabelle syntax observes the following rules for
   1.212 +  representing an indexname @{text "(x, i)"} as a packed string:
   1.213  
   1.214    \begin{itemize}
   1.215  
   1.216 @@ -605,20 +609,15 @@
   1.217  
   1.218    \item @{text "?xi"} if @{text "x"} does not end with a digit,
   1.219  
   1.220 -  \item @{text "?x.i"} else.
   1.221 +  \item @{text "?x.i"} otherwise.
   1.222  
   1.223    \end{itemize}
   1.224  
   1.225 -  Occasionally, basic names and indexed names are injected into the
   1.226 -  same pair type: the (improper) indexname @{text "(x, -1)"} is used
   1.227 -  to encode basic names.
   1.228 -
   1.229 -  \medskip Indexnames may acquire arbitrary large index numbers over
   1.230 -  time.  Results are usually normalized towards @{text "0"} at certain
   1.231 -  checkpoints, such that the very end of a proof.  This works by
   1.232 -  producing variants of the corresponding basic names
   1.233 -  (\secref{sec:basic-names}).  For example, the collection @{text
   1.234 -  "?x.1, ?x.7, ?x.42"} then becomes @{text "?x, ?xa, ?xb"}.
   1.235 +  Indexnames may acquire large index numbers over time.  Results are
   1.236 +  normalized towards @{text "0"} at certain checkpoints, notably at
   1.237 +  the end of a proof.  This works by producing variants of the
   1.238 +  corresponding basic name components.  For example, the collection
   1.239 +  @{text "?x1, ?x7, ?x42"} becomes @{text "?x, ?xa, ?xb"}.
   1.240  *}
   1.241  
   1.242  text %mlref {*
   1.243 @@ -631,7 +630,7 @@
   1.244    \item @{ML_type indexname} represents indexed names.  This is an
   1.245    abbreviation for @{ML_type "string * int"}.  The second component is
   1.246    usually non-negative, except for situations where @{text "(x, -1)"}
   1.247 -  is used to embed plain names.
   1.248 +  is used to embed basic names into this type.
   1.249  
   1.250    \end{description}
   1.251  *}
   1.252 @@ -641,62 +640,61 @@
   1.253  
   1.254  text {*
   1.255    A \emph{qualified name} consists of a non-empty sequence of basic
   1.256 -  name components.  The packed representation a dot as separator, for
   1.257 -  example in ``@{text "A.b.c"}''.  The last component is called
   1.258 -  \emph{base} name, the remaining prefix \emph{qualifier} (which may
   1.259 -  be empty).  The basic idea of qualified names is to encode a
   1.260 -  hierarchically structured name spaces by recording the access path
   1.261 -  as part of the name.  For example, @{text "A.b.c"} may be understood
   1.262 -  as a local entity @{text "c"} within a local structure @{text "b"}
   1.263 -  of the enclosing structure @{text "A"}.  Typically, name space
   1.264 -  hierarchies consist of 1--3 levels, but this need not be always so.
   1.265 +  name components.  The packed representation uses a dot as separator,
   1.266 +  as in ``@{text "A.b.c"}''.  The last component is called \emph{base}
   1.267 +  name, the remaining prefix \emph{qualifier} (which may be empty).
   1.268 +  The idea of qualified names is to encode nested structures by
   1.269 +  recording the access paths as qualifiers.  For example, an item
   1.270 +  named ``@{text "A.b.c"}'' may be understood as a local entity @{text
   1.271 +  "c"}, within a local structure @{text "b"}, within a global
   1.272 +  structure @{text "A"}.  Typically, name space hierarchies consist of
   1.273 +  1--2 levels of qualification, but this need not be always so.
   1.274  
   1.275    The empty name is commonly used as an indication of unnamed
   1.276 -  entities, if this makes any sense.  The operations on qualified
   1.277 -  names are smart enough to pass through such improper names
   1.278 +  entities, whenever this makes any sense.  The basic operations on
   1.279 +  qualified names are smart enough to pass through such improper names
   1.280    unchanged.
   1.281  
   1.282    \medskip A @{text "naming"} policy tells how to turn a name
   1.283    specification into a fully qualified internal name (by the @{text
   1.284 -  "full"} operation), and how to fully qualified names may be accessed
   1.285 -  externally.  For example, the default naming prefixes an implicit
   1.286 -  path from the context: @{text "x"} is becomes @{text "path.x"}
   1.287 -  internally; the standard accesses include @{text "x"}, @{text
   1.288 -  "path.x"}, and further partial @{text "path"} specifications.
   1.289 -  Normally, the naming is implicit in the theory or proof context.
   1.290 -  There are separate versions of the corresponding operations for
   1.291 -  these context types.
   1.292 +  "full"} operation), and how fully qualified names may be accessed
   1.293 +  externally.  For example, the default naming policy is to prefix an
   1.294 +  implicit path: @{text "full x"} produces @{text "path.x"}, and the
   1.295 +  standard accesses for @{text "path.x"} include both @{text "x"} and
   1.296 +  @{text "path.x"}.  Normally, the naming is implicit in the theory or
   1.297 +  proof context; there are separate versions of the corresponding.
   1.298  
   1.299    \medskip A @{text "name space"} manages a collection of fully
   1.300    internalized names, together with a mapping between external names
   1.301    and internal names (in both directions).  The corresponding @{text
   1.302    "intern"} and @{text "extern"} operations are mostly used for
   1.303    parsing and printing only!  The @{text "declare"} operation augments
   1.304 -  a name space according to a given naming policy.
   1.305 +  a name space according to the accesses determined by the naming
   1.306 +  policy.
   1.307  
   1.308 -  By general convention, there are separate name spaces for each kind
   1.309 -  of formal entity, such as logical constant, type, type class,
   1.310 -  theorem etc.  It is usually clear from the occurrence in concrete
   1.311 -  syntax (or from the scope) which kind of entity a name refers to.
   1.312 -  For example, the very same name @{text "c"} may be used uniformly
   1.313 -  for a constant, type, type class, which are from separate syntactic
   1.314 -  categories.
   1.315 +  \medskip As a general principle, there is a separate name space for
   1.316 +  each kind of formal entity, e.g.\ logical constant, type
   1.317 +  constructor, type class, theorem.  It is usually clear from the
   1.318 +  occurrence in concrete syntax (or from the scope) which kind of
   1.319 +  entity a name refers to.  For example, the very same name @{text
   1.320 +  "c"} may be used uniformly for a constant, type constructor, and
   1.321 +  type class.
   1.322  
   1.323    There are common schemes to name theorems systematically, according
   1.324 -  to the name of the main logical entity being involved, such as
   1.325 -  @{text "c.intro"} and @{text "c.elim"} for theorems related to
   1.326 -  constant @{text "c"}.  This technique of mapping names from one
   1.327 -  space into another requires some care in order to avoid conflicts.
   1.328 -  In particular, theorem names derived from type or class names are
   1.329 -  better suffixed in addition to the usual qualification, e.g.\ @{text
   1.330 -  "c_type.intro"} and @{text "c_class.intro"} for theorems related to
   1.331 -  type @{text "c"} and class @{text "c"}, respectively.
   1.332 +  to the name of the main logical entity involved, e.g.\ @{text
   1.333 +  "c.intro"} for a canonical theorem related to constant @{text "c"}.
   1.334 +  This technique of mapping names from one space into another requires
   1.335 +  some care in order to avoid conflicts.  In particular, theorem names
   1.336 +  derived from a type constructor or type class are better suffixed in
   1.337 +  addition to the usual qualification, e.g.\ @{text "c_type.intro"}
   1.338 +  and @{text "c_class.intro"} for theorems related to type @{text "c"}
   1.339 +  and class @{text "c"}, respectively.
   1.340  *}
   1.341  
   1.342  text %mlref {*
   1.343    \begin{mldecls}
   1.344    @{index_ML NameSpace.base: "string -> string"} \\
   1.345 -  @{index_ML NameSpace.drop_base: "string -> string"} \\
   1.346 +  @{index_ML NameSpace.drop_base: "string -> string"} \\  %FIXME qualifier
   1.347    @{index_ML NameSpace.append: "string -> string -> string"} \\
   1.348    @{index_ML NameSpace.pack: "string list -> string"} \\
   1.349    @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
   1.350 @@ -723,9 +721,9 @@
   1.351    \item @{ML NameSpace.append}~@{text "name\<^isub>1 name\<^isub>2"}
   1.352    appends two qualified names.
   1.353  
   1.354 -  \item @{ML NameSpace.pack}~@{text "name"} and @{text
   1.355 -  "NameSpace.unpack"}~@{text "names"} convert between the packed
   1.356 -  string representation and explicit list form of qualified names.
   1.357 +  \item @{ML NameSpace.pack}~@{text "name"} and @{ML
   1.358 +  NameSpace.unpack}~@{text "names"} convert between the packed string
   1.359 +  representation and the explicit list form of qualified names.
   1.360  
   1.361    \item @{ML_type NameSpace.naming} represents the abstract concept of
   1.362    a naming policy.
   1.363 @@ -735,7 +733,7 @@
   1.364    consisting of the theory name.
   1.365  
   1.366    \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
   1.367 -  naming policy by extending its path.
   1.368 +  naming policy by extending its path component.
   1.369  
   1.370    \item @{ML NameSpace.full}@{text "naming name"} turns a name
   1.371    specification (usually a basic name) into the fully qualified
   1.372 @@ -744,26 +742,26 @@
   1.373    \item @{ML_type NameSpace.T} represents name spaces.
   1.374  
   1.375    \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text
   1.376 -  "(space\<^isub>1, space\<^isub>2)"} provide basic operations for
   1.377 -  building name spaces in accordance to the usual theory data
   1.378 -  management (\secref{sec:context-data}).
   1.379 +  "(space\<^isub>1, space\<^isub>2)"} are the canonical operations for
   1.380 +  maintaining name spaces according to theory data management
   1.381 +  (\secref{sec:context-data}).
   1.382  
   1.383    \item @{ML NameSpace.declare}~@{text "naming name space"} enters a
   1.384 -  fully qualified name into the name space, with partial accesses
   1.385 -  being derived from the given policy.
   1.386 +  fully qualified name into the name space, with external accesses
   1.387 +  determined by the naming policy.
   1.388  
   1.389    \item @{ML NameSpace.intern}~@{text "space name"} internalizes a
   1.390    (partially qualified) external name.
   1.391  
   1.392 -  This operation is mostly for parsing.  Note that fully qualified
   1.393 +  This operation is mostly for parsing!  Note that fully qualified
   1.394    names stemming from declarations are produced via @{ML
   1.395 -  "NameSpace.full"} (or derivatives for @{ML_type theory} or @{ML_type
   1.396 -  Proof.context}).
   1.397 +  "NameSpace.full"} (or its derivatives for @{ML_type theory} and
   1.398 +  @{ML_type Proof.context}).
   1.399  
   1.400    \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
   1.401    (fully qualified) internal name.
   1.402  
   1.403 -  This operation is mostly for printing.  Note unqualified names are
   1.404 +  This operation is mostly for printing!  Note unqualified names are
   1.405    produced via @{ML NameSpace.base}.
   1.406  
   1.407    \end{description}
     2.1 --- a/doc-src/IsarImplementation/implementation.tex	Wed Sep 06 22:48:36 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/implementation.tex	Thu Sep 07 15:16:26 2006 +0200
     2.3 @@ -32,7 +32,8 @@
     2.4    We describe the key concepts underlying the Isabelle/Isar
     2.5    implementation, including ML references for the most important
     2.6    functions.  The aim is to give some insight into the overall system
     2.7 -  architecture, and provide clues on implementing user extensions.
     2.8 +  architecture, and provide clues on implementing applications within
     2.9 +  this framework.
    2.10  \end{abstract}
    2.11  
    2.12  \vspace*{2.5cm}