doc-src/IsarRef/Thy/document/Spec.tex
author wenzelm
Fri May 09 23:35:57 2008 +0200 (2008-05-09)
changeset 26869 3bc332135aa7
child 26870 94bedbb34b92
permissions -rw-r--r--
added chapters for "Specifications" and "Proofs";
wenzelm@26869
     1
%
wenzelm@26869
     2
\begin{isabellebody}%
wenzelm@26869
     3
\def\isabellecontext{Spec}%
wenzelm@26869
     4
%
wenzelm@26869
     5
\isadelimtheory
wenzelm@26869
     6
\isanewline
wenzelm@26869
     7
\isanewline
wenzelm@26869
     8
%
wenzelm@26869
     9
\endisadelimtheory
wenzelm@26869
    10
%
wenzelm@26869
    11
\isatagtheory
wenzelm@26869
    12
\isacommand{theory}\isamarkupfalse%
wenzelm@26869
    13
\ Spec\isanewline
wenzelm@26869
    14
\isakeyword{imports}\ Main\isanewline
wenzelm@26869
    15
\isakeyword{begin}%
wenzelm@26869
    16
\endisatagtheory
wenzelm@26869
    17
{\isafoldtheory}%
wenzelm@26869
    18
%
wenzelm@26869
    19
\isadelimtheory
wenzelm@26869
    20
%
wenzelm@26869
    21
\endisadelimtheory
wenzelm@26869
    22
%
wenzelm@26869
    23
\isamarkupchapter{Specifications%
wenzelm@26869
    24
}
wenzelm@26869
    25
\isamarkuptrue%
wenzelm@26869
    26
%
wenzelm@26869
    27
\isadelimtheory
wenzelm@26869
    28
%
wenzelm@26869
    29
\endisadelimtheory
wenzelm@26869
    30
%
wenzelm@26869
    31
\isatagtheory
wenzelm@26869
    32
\isacommand{end}\isamarkupfalse%
wenzelm@26869
    33
%
wenzelm@26869
    34
\endisatagtheory
wenzelm@26869
    35
{\isafoldtheory}%
wenzelm@26869
    36
%
wenzelm@26869
    37
\isadelimtheory
wenzelm@26869
    38
%
wenzelm@26869
    39
\endisadelimtheory
wenzelm@26869
    40
\isanewline
wenzelm@26869
    41
\end{isabellebody}%
wenzelm@26869
    42
%%% Local Variables:
wenzelm@26869
    43
%%% mode: latex
wenzelm@26869
    44
%%% TeX-master: "root"
wenzelm@26869
    45
%%% End: