src/CTT/document/root.tex
author wenzelm
Tue, 09 Mar 2021 21:11:05 +0100
changeset 73404 299f6a8faccc
parent 63505 42e1dece537a
permissions -rw-r--r--
proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 63505
diff changeset
     2
\usepackage[T1]{fontenc}
63505
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     3
\usepackage{isabelle,isabellesym}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     4
\usepackage{pdfsetup}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     5
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     6
\urlstyle{rm}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     7
\isabellestyle{it}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     8
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
     9
\begin{document}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    10
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    11
\title{Isabelle/CTT --- Constructive Type Theory \\
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    12
  with extensional equality and without universes}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    13
\author{Larry Paulson}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    14
\maketitle
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    15
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    16
\tableofcontents
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    17
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    18
\parindent 0pt\parskip 0.5ex
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    19
\input{session}
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    20
42e1dece537a misc tuning and modernization;
wenzelm
parents:
diff changeset
    21
\end{document}