1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Jul 31 21:14:20 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Sat Jul 31 23:32:05 2010 +0200
     1.3 @@ -407,7 +407,7 @@
     1.4  
     1.5    \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
     1.6    constraint @{text \<tau>} on the local parameter @{text x}.  This
     1.7 -  element is deprecated.  The type constaint should be introduced in
     1.8 +  element is deprecated.  The type constraint should be introduced in
     1.9    the for clause or the relevant @{element "fixes"} element.
    1.10  
    1.11    \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
    1.12 @@ -501,7 +501,7 @@
    1.13      ;
    1.14      'interpretation' localeepxr equations?
    1.15      ;
    1.16 -    'interpret' localeexpr
    1.17 +    'interpret' localeexpr equations?
    1.18      ;
    1.19      'print\_interps' nameref
    1.20      ;
    1.21 @@ -560,14 +560,16 @@
    1.22    interpretations dynamically participate in any facts added to
    1.23    locales.
    1.24  
    1.25 -  \item @{command "interpret"}~@{text "expr"}
    1.26 -  interprets @{text expr} in the proof context and is otherwise
    1.27 -  similar to interpretation in theories.
    1.28 +  \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
    1.29 +  @{text expr} in the proof context and is otherwise similar to
    1.30 +  interpretation in theories.  Note that rewrite rules given to
    1.31 +  @{command "interpret"} should be explicitly universally quantified.
    1.32  
    1.33    \item @{command "print_interps"}~@{text "locale"} lists all
    1.34 -  interpretations of @{text "locale"} in the current theory, including
    1.35 -  those due to a combination of an @{command "interpretation"} and
    1.36 -  one or several @{command "sublocale"} declarations.
    1.37 +  interpretations of @{text "locale"} in the current theory or proof
    1.38 +  context, including those due to a combination of a @{command
    1.39 +  "interpretation"} or @{command "interpret"} and one or several
    1.40 +  @{command "sublocale"} declarations.
    1.41  
    1.42    \end{description}
    1.43  
    1.44 @@ -581,7 +583,7 @@
    1.45    \end{warn}
    1.46  
    1.47    \begin{warn}
    1.48 -    An interpretation in a theory may subsume previous
    1.49 +    An interpretation in a theory or proof context may subsume previous
    1.50      interpretations.  This happens if the same specification fragment
    1.51      is interpreted twice and the instantiation of the second
    1.52      interpretation is more general than the interpretation of the