diff --git a/appendix/proof-example.tex b/appendix/proof-example.tex
new file mode 100644
index 0000000..923cb52
--- /dev/null
+++ b/appendix/proof-example.tex
@@ -0,0 +1,4 @@
+% Proof of Theorem~\ref{thm:example}: in the body in the full version, in the appendix in the conference version (macros/version.tex).
+\begin{proof}
+Placeholder proof.
+\end{proof}
diff --git a/appendix/proofs.tex b/appendix/proofs.tex
index 70b1e1f..cd2c751 100644
--- a/appendix/proofs.tex
+++ b/appendix/proofs.tex
@@ -1,2 +1,5 @@
 \section{Proofs}\label{app:proofs}
 % The complete proofs of the results stated in the body.
+
+% In the conference version, each theorem whose proof the full version has in the body is restated here with its proof.  A proof that is in the appendix in both versions goes after them, as it is.
+\appendixproof{examplethm}{proof-example}
diff --git a/macros/theorems.tex b/macros/theorems.tex
index 8d8665a..250a377 100644
--- a/macros/theorems.tex
+++ b/macros/theorems.tex
@@ -1,4 +1,4 @@
-% Theorem environments.  The proof environment is the one amsthm defines.
+% Theorem environments.  The proof environment is the one amsthm defines; thmtools provides the restatable environment that macros/version.tex uses to restate a theorem in the appendix.
 \usepackage{amsthm}
 
 \theoremstyle{plain}
@@ -8,3 +8,5 @@
 
 \theoremstyle{definition}
 \newtheorem{definition}[theorem]{Definition}
+
+\usepackage{thmtools}
diff --git a/macros/version.tex b/macros/version.tex
new file mode 100644
index 0000000..8af6a6c
--- /dev/null
+++ b/macros/version.tex
@@ -0,0 +1,8 @@
+% Full and conference versions.  The full version is the text, and \iffull, defined at the top of main.tex, is true in it.  Text of the full version only goes in \iffull ... \fi; a passage that hiding cannot handle, such as an abstract that differs as a whole, goes in \full{<full>}{<conference>}.
+
+\newcommand{\full}[2]{\iffull#1\else#2\fi}
+
+% A proof is written once, in its own file appendix/<file>.tex, and its theorem is a restatable environment (thmtools).  \proofhere{<file>}, right after the theorem in the body, reads the proof there in the full version and points to the appendix in the conference version.  \appendixproof{<restatable name>}{<file>}, in appendix/proofs.tex, restates the theorem and reads the proof there in the conference version, and does nothing in the full version.
+
+\newcommand{\proofhere}[1]{\iffull\input{appendix/#1}\else\noindent The proof is in Appendix~\ref{app:proofs}.\fi}
+\newcommand{\appendixproof}[2]{\iffull\else\csname #1\endcsname*\input{appendix/#2}\fi}
diff --git a/main.tex b/main.tex
index d509b46..2bf12e0 100644
--- a/main.tex
+++ b/main.tex
@@ -1,7 +1,17 @@
+% ===== Version switch ========================================================
+% The full version is the text.  make conf defines \conference before reading this file and builds the conference version; vimtex, make watch and make full build the full version.  macros/version.tex defines the commands that hide or swap text in the conference version.
+\newif\iffull
+\ifdefined\conference \fullfalse \else \fulltrue \fi
+
 % ===== Document class: article by default ===================================
-% To switch to a venue class, put its files in venue/ (.latexmkrc adds venue/ to the TeX search path), comment out the article line and uncomment the venue line.  A venue class that defines its own theorem environments replaces macros/theorems.tex.
+% To switch a version to a venue class, put the class files in venue/ (.latexmkrc adds venue/ to the TeX search path), comment out the article line of that version and uncomment its venue line.  A venue class that defines its own theorem environments replaces macros/theorems.tex.
+\iffull
 \documentclass[11pt]{article}
 % \documentclass{llncs}
+\else
+\documentclass[11pt]{article}
+% \documentclass{llncs}
+\fi
 % ===== End of document class ================================================
 
 \usepackage[T1]{fontenc}
@@ -13,10 +23,13 @@
 \input{macros/theorems}
 \input{macros/algorithms}
 \input{macros/notation}
+\input{macros/version}
 
 \usepackage[backend=biber,style=numeric-comp]{biblatex}
 \addbibresource{bib/dblp.bib}
 \addbibresource{bib/refs.bib}
+% make conf reads this label to print the page on which the References heading lands.
+\defbibheading{bibliography}[\refname]{\section*{#1}\label{references}}
 
 \usepackage{hyperref}
 
@@ -29,6 +42,7 @@
 \maketitle
 
 \begin{abstract}
+% Sentences of the full version only go in \iffull ... \fi; an abstract that differs as a whole goes in \full{<full abstract>}{<conference abstract>}.
 Abstract.
 \end{abstract}
 
diff --git a/sections/04-security.tex b/sections/04-security.tex
index 4f1b011..d69043a 100644
--- a/sections/04-security.tex
+++ b/sections/04-security.tex
@@ -1,2 +1,7 @@
 \section{Security}\label{sec:security}
 % The security theorems, with their proofs here or in the appendix.
+
+\begin{restatable}{theorem}{examplethm}\label{thm:example}
+Placeholder theorem.
+\end{restatable}
+\proofhere{proof-example}