src/Doc/IsarRef/document/root.tex
author wenzelm
Tue, 28 Aug 2012 18:57:32 +0200
changeset 48985 5386df44a037
parent 48958 doc-src/IsarRef/document/root.tex@12afbf6eb7f9
child 50109 c13dc0b1841c
permissions -rw-r--r--
renamed doc-src to src/Doc; renamed TutorialI to Tutorial;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7836
7a9270282fd3 a4paper;
wenzelm
parents: 7532
diff changeset
     1
\documentclass[12pt,a4paper,fleqn]{report}
28838
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     2
\usepackage{amssymb}
48171
28a6d67c93f0 default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents: 48057
diff changeset
     3
\usepackage{eurosym}
28a6d67c93f0 default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents: 48057
diff changeset
     4
\usepackage[english]{babel}
28838
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     5
\usepackage[only,bigsqcap]{stmaryrd}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     6
\usepackage{textcomp}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     7
\usepackage{latexsym}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     8
\usepackage{graphicx}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
     9
\let\intorig=\int  %iman.sty redefines \int
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    10
\usepackage{iman,extra,isar,proof}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    11
\usepackage[nohyphen,strings]{underscore}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    12
\usepackage{isabelle}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    13
\usepackage{isabellesym}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    14
\usepackage{railsetup}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    15
\usepackage{ttbox}
28773
39b4cedb8433 updated and elaborated Pure grammer;
wenzelm
parents: 28762
diff changeset
    16
\usepackage{supertabular}
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents: 18021
diff changeset
    17
\usepackage{style}
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    18
\usepackage{pdfsetup}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    19
26741
eb15fd4cd1ad converted intro.tex to Thy/intro.thy;
wenzelm
parents: 26738
diff changeset
    20
\hyphenation{Isabelle}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy;
wenzelm
parents: 26738
diff changeset
    21
\hyphenation{Isar}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy;
wenzelm
parents: 26738
diff changeset
    22
eb15fd4cd1ad converted intro.tex to Thy/intro.thy;
wenzelm
parents: 26738
diff changeset
    23
\isadroptag{theory}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    24
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    25
\author{\emph{Makarius Wenzel} \\[3ex]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    26
  With Contributions by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    27
  Clemens Ballarin,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    28
  Stefan Berghofer, \\
44966
1db165e0bd97 more contributors;
wenzelm
parents: 42917
diff changeset
    29
  Jasmin Blanchette,
30569
696f93184f0d tuned interpunctation
haftmann
parents: 30242
diff changeset
    30
  Timothy Bourke,
44966
1db165e0bd97 more contributors;
wenzelm
parents: 42917
diff changeset
    31
  Lukas Bulwahn, \\
27038
854c61598628 more contributors;
wenzelm
parents: 27037
diff changeset
    32
  Lucas Dixon,
44966
1db165e0bd97 more contributors;
wenzelm
parents: 42917
diff changeset
    33
  Florian Haftmann,
47860
fa7f5755b27a more contributors;
wenzelm
parents: 44966
diff changeset
    34
  Brian Huffman, \\
fa7f5755b27a more contributors;
wenzelm
parents: 44966
diff changeset
    35
  Gerwin Klein,
27038
854c61598628 more contributors;
wenzelm
parents: 27037
diff changeset
    36
  Alexander Krauss,
47860
fa7f5755b27a more contributors;
wenzelm
parents: 44966
diff changeset
    37
  Ond\v{r}ej Kun\v{c}ar, \\
44966
1db165e0bd97 more contributors;
wenzelm
parents: 42917
diff changeset
    38
  Tobias Nipkow,
47860
fa7f5755b27a more contributors;
wenzelm
parents: 44966
diff changeset
    39
  Lars Noschinski,
fa7f5755b27a more contributors;
wenzelm
parents: 44966
diff changeset
    40
  David von Oheimb, \\
27038
854c61598628 more contributors;
wenzelm
parents: 27037
diff changeset
    41
  Larry Paulson,
44966
1db165e0bd97 more contributors;
wenzelm
parents: 42917
diff changeset
    42
  Sebastian Skalberg
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    43
}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    44
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    45
\makeindex
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    46
18021
99d170aebb6e literal facts;
wenzelm
parents: 13048
diff changeset
    47
\chardef\charbackquote=`\`
99d170aebb6e literal facts;
wenzelm
parents: 13048
diff changeset
    48
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
99d170aebb6e literal facts;
wenzelm
parents: 13048
diff changeset
    49
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    50
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    51
\begin{document}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    52
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    53
\maketitle 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    54
42915
f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents: 42632
diff changeset
    55
\pagenumbering{roman}
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    56
{\def\isamarkupchapter#1{\chapter*{#1}}\input{Preface.tex}}
42915
f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents: 42632
diff changeset
    57
\tableofcontents
f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents: 42632
diff changeset
    58
\clearfirst
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    59
29718
cf48beb23a70 added parts;
wenzelm
parents: 29716
diff changeset
    60
\part{Basic Concepts}
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    61
\input{Synopsis.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    62
\input{Framework.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    63
\input{First_Order_Logic.tex}
29718
cf48beb23a70 added parts;
wenzelm
parents: 29716
diff changeset
    64
\part{General Language Elements}
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    65
\input{Outer_Syntax.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    66
\input{Document_Preparation.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    67
\input{Spec.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    68
\input{Proof.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    69
\input{Inner_Syntax.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    70
\input{Misc.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    71
\input{Generic.tex}
48957
c04001b3a753 removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;
wenzelm
parents: 48956
diff changeset
    72
\part{Object-Logic}
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    73
\input{HOL_Specific.tex}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    74
29718
cf48beb23a70 added parts;
wenzelm
parents: 29716
diff changeset
    75
\part{Appendix}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7836
diff changeset
    76
\appendix
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    77
\input{Quick_Reference.tex}
28838
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents: 28773
diff changeset
    78
\let\int\intorig
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    79
\input{Symbols.tex}
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    80
\input{ML_Tactic.tex}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7836
diff changeset
    81
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    82
\begingroup
48057
72197611f1e9 use \tocentry as in implementation manual;
wenzelm
parents: 47860
diff changeset
    83
  \tocentry{\bibname}
30116
1fb1833cb199 \bibliographystyle{abbrv} for newer ref manuals;
wenzelm
parents: 29730
diff changeset
    84
  \bibliographystyle{abbrv} \small\raggedright\frenchspacing
48958
12afbf6eb7f9 more standard document preparation within session context;
wenzelm
parents: 48957
diff changeset
    85
  \bibliography{manual}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    86
\endgroup
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    87
48057
72197611f1e9 use \tocentry as in implementation manual;
wenzelm
parents: 47860
diff changeset
    88
\tocentry{\indexname}
8828
5be2d1745c61 improved indexing;
wenzelm
parents: 8596
diff changeset
    89
\printindex
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    90
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    91
\end{document}