doc-src/IsarImplementation/Thy/document/locale.tex
changeset 30130 e23770bc97c8
parent 30129 419116f1157a
parent 30114 0726792e1726
child 30131 6be1be402ef0
--- a/doc-src/IsarImplementation/Thy/document/locale.tex	Thu Feb 26 08:44:44 2009 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{locale}%
-%
-\isadelimtheory
-\isanewline
-\isanewline
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Structured specifications%
-}
-\isamarkuptrue%
-%
-\isamarkupsection{Specification elements%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Type-inference%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Local theories%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-  \glossary{Local theory}{FIXME}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: