tuned;
authorwenzelm
Tue Jul 31 19:38:33 2007 +0200 (2007-07-31)
changeset 24090ab6f04807005
parent 24089 070d539ba403
child 24091 109f19a13872
tuned;
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
src/HOL/IntArith.thy
     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)"