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, 04 Nov 2011 17:19:33 +0100
changeset 45340 98ec8b51af9c
parent 43564 9864182c6bad
child 48895 4cd4ef1ef4a4
permissions -rw-r--r--
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
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{uses}\ {\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
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    14
 
\isakeyword{begin}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    15
 
\endisatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    16
 
{\isafoldtheory}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    17
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    18
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    19
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    20
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    21
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    22
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    23
 
\isadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    24
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    25
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    26
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    27
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    28
 
\isatagML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    29
 
\isacommand{setup}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    30
 
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ Antiquote{\isaliteral{5F}{\isacharunderscore}}Setup{\isaliteral{2E}{\isachardot}}setup\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    31
 
\endisatagML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    32
 
{\isafoldML}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    33
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    34
 
\isadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    35
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    36
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    37
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    38
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    39
 
\isacommand{declare}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    40
 
\ {\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 
    41
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    42
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    43
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    44
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    45
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    46
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    47
 
\isatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    48
 
\isacommand{end}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    49
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    50
 
\endisatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    51
 
{\isafoldtheory}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    52
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    53
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    54
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    55
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    56
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    57
 
\end{isabellebody}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    58
 
%%% Local Variables:
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    59
 
%%% mode: latex
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    60
 
%%% TeX-master: "root"
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
diff changeset 
    61
 
%%% End:
isabelle