doc-src/ProgProve/Thys/document/LaTeXsugar.tex
author wenzelm
Wed, 22 Aug 2012 22:55:41 +0200
changeset 48891 c0eafbd55de3
parent 47269 29aa0c071875
permissions -rw-r--r--
prefer ML_file over old uses;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
\begin{isabellebody}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
\def\isabellecontext{LaTeXsugar}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
\isadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
\isanewline
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
\endisadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
\isatagtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
\endisatagtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
{\isafoldtheory}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
\isadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
\endisadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
\isadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
\endisadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    23
\isatagtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    24
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    25
\endisatagtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    26
{\isafoldtheory}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    27
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    28
\isadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    29
%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    30
\endisadelimtheory
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    31
\end{isabellebody}%
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
%%% Local Variables:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
%%% mode: latex
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
%%% TeX-master: "root"
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
%%% End: