doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 26840 ec46381f149d
child 26849 df50bc1249d7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 07 12:38:55 2008 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +%
     1.5 +\begin{isabellebody}%
     1.6 +\def\isabellecontext{HOL{\isacharunderscore}Specific}%
     1.7 +%
     1.8 +\isadelimtheory
     1.9 +\isanewline
    1.10 +\isanewline
    1.11 +%
    1.12 +\endisadelimtheory
    1.13 +%
    1.14 +\isatagtheory
    1.15 +\isacommand{theory}\isamarkupfalse%
    1.16 +\ HOL{\isacharunderscore}Specific\isanewline
    1.17 +\isakeyword{imports}\ HOL\isanewline
    1.18 +\isakeyword{begin}\isanewline
    1.19 +\isanewline
    1.20 +\isacommand{end}\isamarkupfalse%
    1.21 +%
    1.22 +\endisatagtheory
    1.23 +{\isafoldtheory}%
    1.24 +%
    1.25 +\isadelimtheory
    1.26 +\isanewline
    1.27 +%
    1.28 +\endisadelimtheory
    1.29 +\end{isabellebody}%
    1.30 +%%% Local Variables:
    1.31 +%%% mode: latex
    1.32 +%%% TeX-master: "root"
    1.33 +%%% End: