--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 14:12:14 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 26 14:24:26 2011 +0200
@@ -771,6 +771,11 @@
*}
+subsubsection {* Examples *}
+
+text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *}
+
+
section {* Adhoc tuples *}
text {*
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 14:12:14 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 26 14:24:26 2011 +0200
@@ -1089,6 +1089,15 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+See \verb|~~/src/HOL/ex/Records.thy|, for example.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Adhoc tuples%
}
\isamarkuptrue%