1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Aug 08 13:40:24 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Aug 08 13:48:38 2011 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  theory HOL_Specific
     1.5 -imports Base Main
     1.6 +imports Base Main "~~/src/HOL/Library/Old_Recdef"
     1.7  begin
     1.8  
     1.9  chapter {* Isabelle/HOL \label{ch:hol} *}

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Aug 08 13:40:24 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Aug 08 13:48:38 2011 +0200
     2.3 @@ -9,7 +9,7 @@
     2.4  \isatagtheory
     2.5  \isacommand{theory}\isamarkupfalse%
     2.6  \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
     2.7 -\isakeyword{imports}\ Base\ Main\isanewline
     2.8 +\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
     2.9  \isakeyword{begin}%
    2.10  \endisatagtheory
    2.11  {\isafoldtheory}%