Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/System/Thy/document/Base.tex
author wenzelm
Fri, 24 Aug 2012 13:05:14 +0200
changeset 48919 aaca64a7390c
parent 48895 4cd4ef1ef4a4
permissions -rw-r--r--
some markup for inlined files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     1
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     2
 
\begin{isabellebody}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     3
 
\def\isabellecontext{Base}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     4
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     5
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     6
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     7
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     8
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
     9
 
\isatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    10
 
\isacommand{theory}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    11
 
\ Base\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    12
 
\isakeyword{imports}\ Pure\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    13
 
\isakeyword{begin}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    14
 
\endisatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    15
 
{\isafoldtheory}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    16
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    17
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    18
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    19
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    20
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    21
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    22
 
\isadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    23
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    24
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    25
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    26
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    27
 
\isatagML
48895
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset 
    28
 
\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}\isamarkupfalse%
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset 
    29
 
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    30
 
\isacommand{setup}\isamarkupfalse%
48895
4cd4ef1ef4a4 prefer ML_file over old uses;
wenzelm
parents: 43564
diff changeset 
    31
 
\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup%
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    32
 
\endisatagML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    33
 
{\isafoldML}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    34
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    35
 
\isadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    36
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    37
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    38
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    39
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    40
 
\isacommand{declare}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    41
 
\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}source{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    42
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    43
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    44
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    45
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    46
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    47
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    48
 
\isatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    49
 
\isacommand{end}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    50
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    51
 
\endisatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    52
 
{\isafoldtheory}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    53
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    54
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    55
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    56
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    57
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    58
 
\end{isabellebody}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    59
 
%%% Local Variables:
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    60
 
%%% mode: latex
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    61
 
%%% TeX-master: "root"
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    62
 
%%% End:
isabelle