--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Aug 08 13:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Aug 08 13:48:38 2011 +0200
@@ -1,5 +1,5 @@
theory HOL_Specific
-imports Base Main
+imports Base Main "~~/src/HOL/Library/Old_Recdef"
begin
chapter {* Isabelle/HOL \label{ch:hol} *}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Aug 08 13:40:24 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Aug 08 13:48:38 2011 +0200
@@ -9,7 +9,7 @@
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
-\isakeyword{imports}\ Base\ Main\isanewline
+\isakeyword{imports}\ Base\ Main\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{2F}{\isacharslash}}src{\isaliteral{2F}{\isacharslash}}HOL{\isaliteral{2F}{\isacharslash}}Library{\isaliteral{2F}{\isacharslash}}Old{\isaliteral{5F}{\isacharunderscore}}Recdef{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%