src/HOL/Induct/document/root.tex
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 77036 d0151eb9ecb0
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 61993
diff changeset
     2
\usepackage[T1]{fontenc}
61993
89206877f0ee more symbols;
wenzelm
parents: 12185
diff changeset
     3
\usepackage{amssymb}
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     4
\usepackage{isabelle,isabellesym,pdfsetup}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     5
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     6
%for best-style documents ...
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     7
\urlstyle{rm}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     8
\isabellestyle{it}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
     9
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    10
\begin{document}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    11
12185
wenzelm
parents: 11046
diff changeset
    12
\title{Examples of Inductive and Coinductive Definitions in HOL}
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    13
\author{Stefan Berghofer \\ Tobias Nipkow \\ Lawrence C Paulson \\ Markus Wenzel}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    14
\maketitle
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    15
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    16
\begin{abstract}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    17
  This is a collection of small examples to demonstrate Isabelle/HOL's
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    18
  (co)inductive definitions package.  Large examples appear on many other
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    19
  sessions, such as Lambda, IMP, and Auth.
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    20
\end{abstract}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    21
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    22
\tableofcontents
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    23
\newpage
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    24
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    25
\parindent 0pt\parskip 0.5ex
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    26
\input{session}
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    27
77036
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 73404
diff changeset
    28
\bibliographystyle{abbrv}
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 73404
diff changeset
    29
\bibliography{root}
d0151eb9ecb0 more correct and complete bibliography;
wenzelm
parents: 73404
diff changeset
    30
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents:
diff changeset
    31
\end{document}