author wenzelm Tue Jul 31 19:38:33 2007 +0200 (2007-07-31) changeset 24090 ab6f04807005 parent 24089 070d539ba403 child 24091 109f19a13872
tuned;
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Jul 31 19:26:35 2007 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Jul 31 19:38:33 2007 +0200
1.3 @@ -165,8 +165,8 @@
1.4
1.5    Any user-code that works relatively to the present background theory
1.6    is already safe.  Contextual data may be easily stored within the
1.7 -  theory or proof context, thanks to the generic context data concept
1.8 -  of Isabelle/Isar (see \secref{sec:context-data}).  This greatly
1.9 +  theory or proof context, thanks to the generic data concept of
1.10 +  Isabelle/Isar (see \secref{sec:context-data}).  This greatly
1.11    diminishes the demand for global state information in the first
1.12    place.
1.13
1.14 @@ -194,10 +194,10 @@
1.15    values, without any special precautions for multithreading.  Apart
1.16    from the fully general functors for theory and proof data (see
1.17    \secref{sec:context-data}) there are drop-in replacements that
1.18 -  emulate primitive references for the most basic cases of
1.19 -  \emph{configuration options} for type @{ML_type "bool"}/@{ML_type
1.20 -  "int"}/@{ML_type "string"} (see structure @{ML_struct ConfigOption})
1.21 -  and lists of theorems (see functor @{ML_functor NamedThmsFun}).
1.22 +  emulate primitive references for common cases of \emph{configuration
1.23 +  options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
1.24 +  "string"} (see structure @{ML_struct ConfigOption}) and lists of
1.25 +  theorems (see functor @{ML_functor NamedThmsFun}).
1.26
1.27    \item Keep components with local state information
1.28    \emph{re-entrant}.  Instead of poking initial values into (private)
1.29 @@ -214,15 +214,15 @@
1.30    example is the @{ML show_types} flag, which tells the pretty printer
1.31    to output explicit type information for terms.  Such flags usually
1.32    do not affect the functionality of the core system, but only the
1.33 -  output being presented to the user.
1.34 +  view being presented to the user.
1.35
1.36    Occasionally, such global process flags are treated like implicit
1.37    arguments to certain operations, by using the @{ML setmp} combinator
1.38 -  for safe temporary assignment.  Traditionally its main purpose was
1.39 -  to ensure proper recovery of the original value when exceptions are
1.40 -  raised in the body.  Now the functionality is extended to enter the
1.41 -  \emph{critical section}, with its usual potential of degrading
1.42 -  parallelism.
1.43 +  for safe temporary assignment.  Its traditional purpose was to
1.44 +  ensure proper recovery of the original value when exceptions are
1.45 +  raised in the body, now the functionality is extended to enter the
1.46 +  \emph{critical section} (with its usual potential of degrading
1.47 +  parallelism).
1.48
1.49    Note that recovery of plain value passing semantics via @{ML
1.50    setmp}~@{text "ref value"} assumes that this @{text "ref"} is
1.51 @@ -247,10 +247,10 @@
1.52
1.53    Recall that in an open LCF-style'' system like Isabelle/Isar, the
1.54    user participates in constructing the overall environment.  This
1.55 -  means that state-based facilities offered by one component need to
1.56 -  be used with caution later on.  Minimizing critical elements, by
1.57 -  staying within the plain value-oriented view relative to theory or
1.58 -  proof contexts most of the time, will also reduce the chance of
1.59 +  means that state-based facilities offered by one component will
1.60 +  require special caution later on.  So minimizing critical elements,
1.61 +  by staying within the plain value-oriented view relative to theory
1.62 +  or proof contexts most of the time, will also reduce the chance of
1.63    mishaps occurring to end-users.
1.64  *}
1.65
1.66 @@ -264,9 +264,10 @@
1.67    \begin{description}
1.68
1.69    \item @{ML NAMED_CRITICAL}~@{text "name f"} evaluates @{text "f ()"}
1.70 -  while staying within the critical section.  The @{text "name"}
1.71 -  argument serves for diagnostic output and might help to determine
1.72 -  sources of congestion.
1.73 +  while staying within the critical section of Isabelle/Isar.  No
1.74 +  other thread may do so at the same time, but non-critical parallel
1.75 +  execution will continue.  The @{text "name"} argument serves for
1.76 +  diagnostic purposes and might help to spot sources of congestion.
1.77
1.78    \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
1.79    name argument.

     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Jul 31 19:26:35 2007 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Jul 31 19:38:33 2007 +0200
2.3 @@ -187,8 +187,8 @@
2.4
2.5    Any user-code that works relatively to the present background theory
2.6    is already safe.  Contextual data may be easily stored within the
2.7 -  theory or proof context, thanks to the generic context data concept
2.8 -  of Isabelle/Isar (see \secref{sec:context-data}).  This greatly
2.9 +  theory or proof context, thanks to the generic data concept of
2.10 +  Isabelle/Isar (see \secref{sec:context-data}).  This greatly
2.11    diminishes the demand for global state information in the first
2.12    place.
2.13
2.14 @@ -216,9 +216,9 @@
2.15    values, without any special precautions for multithreading.  Apart
2.16    from the fully general functors for theory and proof data (see
2.17    \secref{sec:context-data}) there are drop-in replacements that
2.18 -  emulate primitive references for the most basic cases of
2.19 -  \emph{configuration options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|ConfigOption|)
2.20 -  and lists of theorems (see functor \verb|NamedThmsFun|).
2.21 +  emulate primitive references for common cases of \emph{configuration
2.22 +  options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|ConfigOption|) and lists of
2.23 +  theorems (see functor \verb|NamedThmsFun|).
2.24
2.25    \item Keep components with local state information
2.26    \emph{re-entrant}.  Instead of poking initial values into (private)
2.27 @@ -235,15 +235,15 @@
2.28    example is the \verb|show_types| flag, which tells the pretty printer
2.29    to output explicit type information for terms.  Such flags usually
2.30    do not affect the functionality of the core system, but only the
2.31 -  output being presented to the user.
2.32 +  view being presented to the user.
2.33
2.34    Occasionally, such global process flags are treated like implicit
2.35    arguments to certain operations, by using the \verb|setmp| combinator
2.36 -  for safe temporary assignment.  Traditionally its main purpose was
2.37 -  to ensure proper recovery of the original value when exceptions are
2.38 -  raised in the body.  Now the functionality is extended to enter the
2.39 -  \emph{critical section}, with its usual potential of degrading
2.40 -  parallelism.
2.41 +  for safe temporary assignment.  Its traditional purpose was to
2.42 +  ensure proper recovery of the original value when exceptions are
2.43 +  raised in the body, now the functionality is extended to enter the
2.44 +  \emph{critical section} (with its usual potential of degrading
2.45 +  parallelism).
2.46
2.47    Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is
2.48    exclusively manipulated within the critical section.  In particular,
2.49 @@ -267,10 +267,10 @@
2.50
2.51    Recall that in an open LCF-style'' system like Isabelle/Isar, the
2.52    user participates in constructing the overall environment.  This
2.53 -  means that state-based facilities offered by one component need to
2.54 -  be used with caution later on.  Minimizing critical elements, by
2.55 -  staying within the plain value-oriented view relative to theory or
2.56 -  proof contexts most of the time, will also reduce the chance of
2.57 +  means that state-based facilities offered by one component will
2.58 +  require special caution later on.  So minimizing critical elements,
2.59 +  by staying within the plain value-oriented view relative to theory
2.60 +  or proof contexts most of the time, will also reduce the chance of
2.61    mishaps occurring to end-users.%
2.62  \end{isamarkuptext}%
2.63  \isamarkuptrue%
2.64 @@ -291,9 +291,10 @@
2.65    \begin{description}
2.66
2.67    \item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}}
2.68 -  while staying within the critical section.  The \isa{name}
2.69 -  argument serves for diagnostic output and might help to determine
2.70 -  sources of congestion.
2.71 +  while staying within the critical section of Isabelle/Isar.  No
2.72 +  other thread may do so at the same time, but non-critical parallel
2.73 +  execution will continue.  The \isa{name} argument serves for
2.74 +  diagnostic purposes and might help to spot sources of congestion.
2.75
2.76    \item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
2.77    name argument.

     3.1 --- a/src/HOL/IntArith.thy	Tue Jul 31 19:26:35 2007 +0200
3.2 +++ b/src/HOL/IntArith.thy	Tue Jul 31 19:38:33 2007 +0200
3.3 @@ -14,10 +14,6 @@
3.4    ("int_arith1.ML")
3.5  begin
3.6
3.7 -text{*Duplicate: can't understand why it's necessary*}
3.8 -declare numeral_0_eq_0 [simp]
3.9 -
3.10 -
3.11  subsection{*Inequality Reasoning for the Arithmetic Simproc*}
3.12
3.13  lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)"