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/IsarImplementation/Thy/document/Base.tex
author wenzelm
Thu, 23 Aug 2012 19:57:55 +0200
changeset 48912 ffdb37019b2f
parent 48895 4cd4ef1ef4a4
permissions -rw-r--r--
improved errors of parser combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     1
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     2
 
\begin{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     3
 
\def\isabellecontext{Base}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     4
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     5
 
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     6
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     7
 
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     8
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
     9
 
\isatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    10
 
\isacommand{theory}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    11
 
\ Base\isanewline
39885
6a3f7941c3a0 cumulative update of generated files (since bf164c153d10);
wenzelm
parents: 30296
diff changeset 
    12
 
\isakeyword{imports}\ Main\isanewline
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    13
 
\isakeyword{begin}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    14
 
\endisatagtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    15
 
{\isafoldtheory}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    16
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    17
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    18
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    19
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    20
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    21
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    22
 
\isadelimML
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    23
 
\isanewline
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    24
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    25
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    26
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
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: 40406
diff changeset 
    30
 
\isacommand{setup}\isamarkupfalse%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    31
 
\ {\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: 40406
diff changeset 
    32
 
\endisatagML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    33
 
{\isafoldML}%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    34
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    35
 
\isadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    36
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    37
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    38
 
\endisadelimML
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    39
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    40
 
\isadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    41
 
\isanewline
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    42
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    43
 
\endisadelimtheory
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    44
 
%
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 40406
diff changeset 
    45
 
\isatagtheory
30296
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    46
 
\isacommand{end}\isamarkupfalse%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    47
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    48
 
\endisatagtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    49
 
{\isafoldtheory}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    50
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    51
 
\isadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    52
 
\isanewline
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    53
 
%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    54
 
\endisadelimtheory
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    55
 
\end{isabellebody}%
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    56
 
%%% Local Variables:
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    57
 
%%% mode: latex
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    58
 
%%% TeX-master: "root"
25eb9a499966 recovered generated files;
wenzelm
parents:
diff changeset 
    59
 
%%% End:
isabelle