Typos in documenation.
authorballarin
Mon Nov 23 21:03:49 2009 +0100 (2009-11-23)
changeset 3386752643d0f856d
parent 33866 34e45b2afe43
child 33868 62251d6b0038
Typos in documenation.
doc-src/IsarRef/Thy/Spec.thy
doc-src/Locales/Locales/Examples3.thy
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 23 19:03:16 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 23 21:03:49 2009 +0100
     1.3 @@ -456,13 +456,10 @@
     1.4    \secref{sec:object-logic}).  Separate introduction rules @{text
     1.5    loc_axioms.intro} and @{text loc.intro} are provided as well.
     1.6    
     1.7 -  \item @{command "print_locale"}~@{text "import + body"} prints the
     1.8 -  specified locale expression in a flattened form.  The notable
     1.9 -  special case @{command "print_locale"}~@{text loc} just prints the
    1.10 -  contents of the named locale, but keep in mind that type-inference
    1.11 -  will normalize type variables according to the usual alphabetical
    1.12 -  order.  The command omits @{element "notes"} elements by default.
    1.13 -  Use @{command "print_locale"}@{text "!"} to get them included.
    1.14 +  \item @{command "print_locale"}~@{text "locale"} prints the
    1.15 +  contents of the named locale.  The command omits @{element "notes"}
    1.16 +  elements by default.  Use @{command "print_locale"}@{text "!"} to
    1.17 +  have them included.
    1.18  
    1.19    \item @{command "print_locales"} prints the names of all locales
    1.20    of the current theory.
    1.21 @@ -537,7 +534,7 @@
    1.22    qualifier, although only for fragments of @{text expr} that are not
    1.23    interpreted in the theory already.
    1.24  
    1.25 -  \item @{command "interpretation"}~@{text "expr insts \<WHERE> eqns"}
    1.26 +  \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
    1.27    interprets @{text expr} in the theory.  The command generates proof
    1.28    obligations for the instantiated specifications (assumes and defines
    1.29    elements).  Once these are discharged by the user, instantiated
    1.30 @@ -563,19 +560,24 @@
    1.31    interpretations dynamically participate in any facts added to
    1.32    locales.
    1.33  
    1.34 -  \item @{command "interpret"}~@{text "expr insts"}
    1.35 +  \item @{command "interpret"}~@{text "expr"}
    1.36    interprets @{text expr} in the proof context and is otherwise
    1.37    similar to interpretation in theories.
    1.38  
    1.39 +  \item @{command "print_interps"}~@{text "locale"} lists all
    1.40 +  interpretations of @{text "locale"} in the current theory, including
    1.41 +  those due to a combination of an @{command "interpretation"} and
    1.42 +  one or several @{command "sublocale"} declarations.
    1.43 +
    1.44    \end{description}
    1.45  
    1.46    \begin{warn}
    1.47      Since attributes are applied to interpreted theorems,
    1.48      interpretation may modify the context of common proof tools, e.g.\
    1.49 -    the Simplifier or Classical Reasoner.  Since the behavior of such
    1.50 -    automated reasoning tools is \emph{not} stable under
    1.51 -    interpretation morphisms, manual declarations might have to be
    1.52 -    added to revert such declarations.
    1.53 +    the Simplifier or Classical Reasoner.  As the behavior of such
    1.54 +    tools is \emph{not} stable under interpretation morphisms, manual
    1.55 +    declarations might have to be added to the target context of the
    1.56 +    interpretation to revert such declarations.
    1.57    \end{warn}
    1.58  
    1.59    \begin{warn}
     2.1 --- a/doc-src/Locales/Locales/Examples3.thy	Mon Nov 23 19:03:16 2009 +0100
     2.2 +++ b/doc-src/Locales/Locales/Examples3.thy	Mon Nov 23 21:03:49 2009 +0100
     2.3 @@ -591,7 +591,7 @@
     2.4    ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\
     2.5    \textit{instance} & ::=
     2.6    & [ \textit{qualifier} ``\textbf{:}'' ]
     2.7 -    \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     2.8 +    \textit{name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\
     2.9    \textit{expression}  & ::= 
    2.10    & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$
    2.11      [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex]
    2.12 @@ -625,8 +625,8 @@
    2.13  
    2.14    \textit{toplevel} & ::=
    2.15    & \textbf{print\_locales} \\
    2.16 -  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\
    2.17 -  & | & \textbf{print\_interps} \textit{locale}
    2.18 +  & | & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{name} \\
    2.19 +  & | & \textbf{print\_interps} \textit{name}
    2.20  \end{tabular}
    2.21  \end{center}
    2.22  \hrule