isabelle: src/Doc/Isar_Ref/document/root.tex@f12a52b5d812 (annotated)

7836 7a9270282fd3 a4paper; wenzelm parents: 7532 diff changeset	1	\documentclass[12pt,a4paper,fleqn]{report}
60185 cc71f01f9fde prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive; wenzelm parents: 59974 diff changeset	2	\usepackage{lmodern}
55365 9d5aba2baa4c yet another attempt at actual underscore; wenzelm parents: 52896 diff changeset	3	\usepackage[T1]{fontenc}
61963 2548e7cc86fb more arrow symbols; wenzelm parents: 61409 diff changeset	4	\usepackage{amsmath}
28838 d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	5	\usepackage{amssymb}
59974 b911c8ba0b69 added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34); wenzelm parents: 57590 diff changeset	6	\usepackage{wasysym}
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	7	\usepackage{eurosym}
69962 82e945d472d5 documentation of document markers and re-interpreted command tags; wenzelm parents: 64511 diff changeset	8	\usepackage{pifont}
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	9	\usepackage[english]{babel}
28838 d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	10	\usepackage[only,bigsqcap]{stmaryrd}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	11	\usepackage{textcomp}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	12	\usepackage{latexsym}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	13	\usepackage{graphicx}
d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	14	\let\intorig=\int %iman.sty redefines \int
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	15	\usepackage{iman,extra,isar,proof}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	16	\usepackage[nohyphen,strings]{underscore}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	17	\usepackage{isabelle}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	18	\usepackage{isabellesym}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	19	\usepackage{railsetup}
28773 39b4cedb8433 updated and elaborated Pure grammer; wenzelm parents: 28762 diff changeset	20	\usepackage{supertabular}
26738 615e1a86787b basic setup for generated document (cf. ../IsarImplementation); wenzelm parents: 18021 diff changeset	21	\usepackage{style}
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	22	\usepackage{pdfsetup}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	23
26741 eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	24	\hyphenation{Isabelle}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	25	\hyphenation{Isar}
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	26
eb15fd4cd1ad converted intro.tex to Thy/intro.thy; wenzelm parents: 26738 diff changeset	27	\isadroptag{theory}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	28	\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
26870 94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	29	\author{\emph{Makarius Wenzel} \\[3ex]
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	30	With Contributions by
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	31	Clemens Ballarin,
94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	32	Stefan Berghofer, \\
44966 1db165e0bd97 more contributors; wenzelm parents: 42917 diff changeset	33	Jasmin Blanchette,
30569 696f93184f0d tuned interpunctation haftmann parents: 30242 diff changeset	34	Timothy Bourke,
44966 1db165e0bd97 more contributors; wenzelm parents: 42917 diff changeset	35	Lukas Bulwahn, \\
50130 8c6fde547cba some documentation for "algebra" in HOL; wenzelm parents: 50109 diff changeset	36	Amine Chaieb,
27038 854c61598628 more contributors; wenzelm parents: 27037 diff changeset	37	Lucas Dixon,
50130 8c6fde547cba some documentation for "algebra" in HOL; wenzelm parents: 50109 diff changeset	38	Florian Haftmann, \\
8c6fde547cba some documentation for "algebra" in HOL; wenzelm parents: 50109 diff changeset	39	Brian Huffman,
57590 06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	40	Lars Hupel,
06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	41	Gerwin Klein, \\
06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	42	Alexander Krauss,
50130 8c6fde547cba some documentation for "algebra" in HOL; wenzelm parents: 50109 diff changeset	43	Ond\v{r}ej Kun\v{c}ar,
57590 06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	44	Andreas Lochbihler, \\
06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	45	Tobias Nipkow,
56364 fbacdc80e1bc more contributors; wenzelm parents: 55366 diff changeset	46	Lars Noschinski,
57590 06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	47	David von Oheimb, \\
06cb5375e189 more on "Simplifier trace" (by Lars Hupel); wenzelm parents: 56451 diff changeset	48	Larry Paulson,
60837 c362049f3f84 more documentation of coercions traytel parents: 60674 diff changeset	49	Sebastian Skalberg, \\
c362049f3f84 more documentation of coercions traytel parents: 60674 diff changeset	50	Christian Sternagel,
c362049f3f84 more documentation of coercions traytel parents: 60674 diff changeset	51	Dmitriy Traytel
26870 94bedbb34b92 misc reorganization; wenzelm parents: 26869 diff changeset	52	}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	53
7050 c70d3402fef5 checkpoint; wenzelm parents: 7046 diff changeset	54	\makeindex
c70d3402fef5 checkpoint; wenzelm parents: 7046 diff changeset	55
18021 99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	56	\chardef\charbackquote=`\`
99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	57	\newcommand{\backquote}{\mbox{\tt\charbackquote}}
99d170aebb6e literal facts; wenzelm parents: 13048 diff changeset	58
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	59
9f755ff43cff skeleton only; wenzelm parents: diff changeset	60	\begin{document}
9f755ff43cff skeleton only; wenzelm parents: diff changeset	61
9f755ff43cff skeleton only; wenzelm parents: diff changeset	62	\maketitle
9f755ff43cff skeleton only; wenzelm parents: diff changeset	63
42915 f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex); wenzelm parents: 42632 diff changeset	64	\pagenumbering{roman}
60286 410115884a92 tuned; wenzelm parents: 59974 diff changeset	65	\chapter*{Preface}
410115884a92 tuned; wenzelm parents: 59974 diff changeset	66	\input{Preface.tex}
42915 f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex); wenzelm parents: 42632 diff changeset	67	\tableofcontents
64511 287d4cdf70a0 tuned; wenzelm parents: 61963 diff changeset	68	\listoffigures
42915 f35aae36cad0 turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex); wenzelm parents: 42632 diff changeset	69	\clearfirst
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	70
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	71	\part{Basic Concepts}
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	72	\input{Synopsis.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	73	\input{Framework.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	74	\input{First_Order_Logic.tex}
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	75	\part{General Language Elements}
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	76	\input{Outer_Syntax.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	77	\input{Document_Preparation.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	78	\input{Spec.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	79	\input{Proof.tex}
60484 98ee86354354 moved sections; wenzelm parents: 60301 diff changeset	80	\input{Proof_Script.tex}
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	81	\input{Inner_Syntax.tex}
12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	82	\input{Generic.tex}
50109 c13dc0b1841c tuned structure of Isabelle/HOL; wenzelm parents: 48985 diff changeset	83	\part{Isabelle/HOL}\label{part:hol}
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	84	\input{HOL_Specific.tex}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	85
29718 cf48beb23a70 added parts; wenzelm parents: 29716 diff changeset	86	\part{Appendix}
7895 7c492d8bc8e3 updated; wenzelm parents: 7836 diff changeset	87	\appendix
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	88	\input{Quick_Reference.tex}
28838 d5db6dfcb34a moved table of standard Isabelle symbols to isar-ref manual; wenzelm parents: 28773 diff changeset	89	\let\int\intorig
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	90	\input{Symbols.tex}
7895 7c492d8bc8e3 updated; wenzelm parents: 7836 diff changeset	91
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	92	\begingroup
48057 72197611f1e9 use \tocentry as in implementation manual; wenzelm parents: 47860 diff changeset	93	\tocentry{\bibname}
30116 1fb1833cb199 \bibliographystyle{abbrv} for newer ref manuals; wenzelm parents: 29730 diff changeset	94	\bibliographystyle{abbrv} \small\raggedright\frenchspacing
48958 12afbf6eb7f9 more standard document preparation within session context; wenzelm parents: 48957 diff changeset	95	\bibliography{manual}
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	96	\endgroup
9f755ff43cff skeleton only; wenzelm parents: diff changeset	97
48057 72197611f1e9 use \tocentry as in implementation manual; wenzelm parents: 47860 diff changeset	98	\tocentry{\indexname}
8828 5be2d1745c61 improved indexing; wenzelm parents: 8596 diff changeset	99	\printindex
7046 9f755ff43cff skeleton only; wenzelm parents: diff changeset	100
9f755ff43cff skeleton only; wenzelm parents: diff changeset	101	\end{document}

author	wenzelm
	Thu, 28 Mar 2019 13:06:32 +0100
changeset 70006	f12a52b5d812
parent 69962	82e945d472d5
child 72319	76bb6dd505c0
permissions	-rw-r--r--