# HG changeset patch
# User wenzelm
# Date 1306412666 -7200
# Node ID 6891e8a8d7485fa11e9946c072f4bd3900bed12a
# Parent  6834af822a8bb3b7ab9f8851bcf5973f87fc90f2
record examples;

diff -r 6834af822a8b -r 6891e8a8d748 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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 {*
diff -r 6834af822a8b -r 6891e8a8d748 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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%