src/HOL/Computational_Algebra/document/root.tex
author haftmann
Fri, 27 Jun 2025 08:09:26 +0200
changeset 82775 61c39a9e5415
parent 80061 4c1347e172b1
permissions -rw-r--r--
typo
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
80061
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     2
\usepackage[T1]{fontenc}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     3
\usepackage{isabelle}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     4
\usepackage{isabellesym}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     5
\usepackage{latexsym}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     6
\usepackage{textcomp}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     7
\usepackage{amsmath}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     8
\usepackage{amssymb}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     9
\usepackage[only,bigsqcap]{stmaryrd}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    10
\usepackage{pdfsetup}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    11
\usepackage{graphicx}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    12
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    13
\urlstyle{rm}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    14
\isabellestyle{it}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    15
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    16
\begin{document}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    17
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    18
\title{Computational Algebra}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    19
\maketitle
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    20
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    21
\tableofcontents
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    22
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    23
\begin{center}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    24
  \includegraphics[width=\textwidth]{session_graph}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    25
\end{center}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    26
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    27
\newpage
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    28
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    29
\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    30
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    31
\parindent 0pt\parskip 0.5ex
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    32
\input{session}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    33
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    34
\pagestyle{headings}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    35
\bibliographystyle{abbrv}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    36
\bibliography{root}
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    37
4c1347e172b1 moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    38
\end{document}