1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 14:12:14 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 26 14:24:26 2011 +0200
     1.3 @@ -771,6 +771,11 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsubsection {* Examples *}
     1.8 +
     1.9 +text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *}
    1.10 +
    1.11 +
    1.12  section {* Adhoc tuples *}
    1.13  
    1.14  text {*

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 14:12:14 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 26 14:24:26 2011 +0200
     2.3 @@ -1089,6 +1089,15 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 +\isamarkupsubsubsection{Examples%
     2.8 +}
     2.9 +\isamarkuptrue%
    2.10 +%
    2.11 +\begin{isamarkuptext}%
    2.12 +See \verb|~~/src/HOL/ex/Records.thy|, for example.%
    2.13 +\end{isamarkuptext}%
    2.14 +\isamarkuptrue%
    2.15 +%
    2.16  \isamarkupsection{Adhoc tuples%
    2.17  }
    2.18  \isamarkuptrue%