33 lines
710 B
TeX
33 lines
710 B
TeX
\input{common.inc}
|
|
|
|
%\setbeamertemplate{footline}{}
|
|
|
|
\setcounter{part}{2}
|
|
\setcounter{framenumber}{291}
|
|
|
|
\begin{document}
|
|
\partstitleframe{Parts III}
|
|
|
|
%\input{00_webpage_intro.tex}
|
|
%\input{01_introduction.tex}
|
|
%\input{02_organisational_matters.tex}
|
|
\input{03_hol_overview.tex}
|
|
%\input{04_hol_logic.tex}
|
|
%\input{05_usage.tex}
|
|
%\input{06_forward_proofs.tex}
|
|
%\input{07_backward_proofs.tex}
|
|
%\input{08_basic_tactics.tex}
|
|
%\input{09_induction.tex}
|
|
%\input{10_definitions.tex}
|
|
%\input{11_good_definitions.tex}
|
|
%\input{12_deep_shallow.tex}
|
|
%\input{13_rewriting.tex}
|
|
%\input{14_advanced_definitions.tex}
|
|
%\input{15_maintainable_proofs.tex}
|
|
%\input{16_hol_overview.tex}
|
|
%\input{17_other_provers.tex}
|
|
|
|
|
|
\end{document}
|
|
|