110 lines
3.4 KiB
PHP
110 lines
3.4 KiB
PHP
\documentclass{beamer}
|
|
|
|
\usepackage{pgf,pgfnodes,pgfarrows}
|
|
\usepackage{amssymb}
|
|
\usepackage{amsmath}
|
|
\usepackage{graphicx}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage{hyperref}
|
|
\usepackage{booktabs}
|
|
\usepackage{mathpartir}
|
|
\usepackage{latexsym}
|
|
\usepackage{textcomp}
|
|
|
|
\newcommand{\ie}{i.\,e.\ }
|
|
\newcommand{\eg}{e.\,g.\ }
|
|
\newcommand{\wrt}{w.\,r.\,t.\ }
|
|
\newcommand{\aka}{a.\,k.\,a.\ }
|
|
\newcommand{\cf}{cf.\ }
|
|
\newcommand{\etc}{etc.\ }
|
|
\newcommand{\cearrow}{\url{~}>}
|
|
\renewcommand{\emph}[1]{\structure{\textbf{#1}}}
|
|
\newcommand{\entails}{\vdash}
|
|
\newcommand{\hol}[1]{\emph{\texttt{#1}}}
|
|
\newcommand{\ml}[1]{\emph{\texttt{#1}}}
|
|
\newcommand{\textbsl}{\char`\\{}}
|
|
\newcommand{\holAnd}{/\textbsl{}}
|
|
\newcommand{\holOr}{\textbsl{}/}
|
|
\newcommand{\holLambda}{\textbsl{}}
|
|
\newcommand{\holImp}{==>}
|
|
\newcommand{\holEquiv}{<=>}
|
|
\newcommand{\holNeg}{\raisebox{0.5ex}{\texttildelow}}
|
|
\newcommand{\mlcomment}[1]{\structure{(* #1 *)}}
|
|
\newcommand{\aequiv}{\ensuremath{\stackrel{\alpha}{\equiv}}\ }
|
|
\newcommand\pro{\item[$+$]}
|
|
\newcommand\con{\item[$-$]}
|
|
|
|
\newcommand{\bottomstatement}[1]{
|
|
\begin{center}
|
|
\textbf{#1}
|
|
\end{center}
|
|
}
|
|
|
|
\input{version.inc}
|
|
|
|
\title{Interactive Theorem Proving (ITP) Course}
|
|
\institute{
|
|
\includegraphics[width=1.25cm]{images/cc/cc.eps}
|
|
\includegraphics[width=1.25cm]{images/cc/by.eps}
|
|
\includegraphics[width=1.25cm]{images/cc/sa.eps}\\
|
|
\scriptsize{Except where otherwise noted, this work is licened under\\
|
|
\href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution-ShareAlike 4.0 International License}}}
|
|
\author{Thomas Tuerk (thomas@tuerk-brechen.de)}
|
|
\date{Academic Year 2016/17, Period 4}
|
|
\newcommand{\partstitle}[1]{\title{Interactive Theorem Proving (ITP) Course\\#1}}
|
|
\newcommand{\titleframe}{\frame[plain]{\titlepage\hfill\tiny version \GITAbrHash{} of \GITAuthorDate{}}}
|
|
\newcommand{\partstitleframe}[1]{\partstitle{#1}\titleframe}
|
|
|
|
|
|
\usetheme{Boadilla}
|
|
\setbeamertemplate{footline}[frame number]{}
|
|
|
|
|
|
\logo{\pgfputat{\pgfxy(-.5,8.7)}{\pgfbox[center,top]{\includegraphics[width=8mm]{images/cc/by-sa.eps}}}}
|
|
|
|
\setbeamertemplate{part page}
|
|
{
|
|
\begin{centering}
|
|
{\usebeamerfont{part name}\usebeamercolor[fg]{part name}\partname~\insertromanpartnumber}
|
|
\vskip1em\par
|
|
\begin{beamercolorbox}[sep=16pt,center]{part title}
|
|
\usebeamerfont{part title}\insertpart\par
|
|
\end{beamercolorbox}
|
|
\vfill
|
|
\begin{center}
|
|
\includegraphics[width=0.75cm]{images/cc/cc.eps}
|
|
\includegraphics[width=0.75cm]{images/cc/by.eps}
|
|
\includegraphics[width=0.75cm]{images/cc/sa.eps}\\
|
|
\tiny{Except where otherwise noted, this work is licened under\\
|
|
\href{http://creativecommons.org/licenses/by-sa/4.0/}{Creative Commons Attribution-ShareAlike 4.0 International License}}.
|
|
\end{center}
|
|
\end{centering}
|
|
}
|
|
|
|
\makeatletter
|
|
\AtBeginPart{%
|
|
\addtocontents{toc}{\protect\beamer@partintoc{\the\c@part}{\beamer@partnameshort}{\the\c@page}{\the\numexpr\value{framenumber}+1\relax}}%
|
|
}
|
|
%% number, shortname, page.
|
|
\providecommand\beamer@partintoc[4]{%
|
|
\ifnum\c@tocdepth=-1\relax
|
|
% requesting onlyparts.
|
|
\qquad\makebox[5em][l]{\hyperlink{page.#3}{\emph{Part {\uppercase\expandafter{\romannumeral #1\relax}}}}} \makebox[18em][l]{\hyperlink{page.#3}{#2}}
|
|
\makebox[3em][r]{\hyperlink{page.#3}{#4}}
|
|
|
|
\par
|
|
\fi
|
|
}
|
|
\define@key{beamertoc}{onlyparts}[]{%
|
|
\c@tocdepth=-1\relax
|
|
}
|
|
\makeatother
|
|
|
|
%\usefonttheme[onlylarge]{structurebold}
|
|
%\usepackage{times}
|
|
|
|
\ifdefined\ttbwflag
|
|
\usecolortheme{seagull}
|
|
\beamertemplatenavigationsymbolsempty
|
|
\fi
|