Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex
===================================================================
--- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision c58bb11d551d74c2ac53af26eaad95ade660e9d5)
+++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex	(revision 0e6a0bebb41b45cf615f928ea49e1295870c1fc7)
@@ -293,5 +293,5 @@
 If the assertions of the minimal-cost top-level interpretation cannot be satisfied then the next-most-minimal-cost interpretation's assertions are checked, and so forth until a minimal-cost satisfiable interpretation (or ambiguous set thereof) is found, or no top-level interpretations are found to have satisfiable assertions. 
 In the common case where the code actually does compile this saves the work of checking assertions for ultimately-rejected interpretations, though it does rule out some pruning opportunities for subinterpretations with unsatisfiable assertions or which are more expensive than a minimal-cost polymorphic function with the same return type. 
-The experimental results in Section~\ref{resn-expr-sec} indicate that this is a worthwhile trade-off. 
+The experimental results in Chapter~\ref{expr-chap} indicate that this is a worthwhile trade-off. 
 
 Optimizing assertion satisfaction for common idioms has also proved effective in \CFA{}; the code below is an unexceptional print statement derived from the \CFA{} test suite that nonetheless is a very difficult instance of expression resolution:
@@ -326,10 +326,4 @@
 As such, I opted to continue Bilson's approach of designing a bespoke solver for \CFA{} assertion satisfaction, rather than attempting to re-express the problem in some more general formalism. 
 
-\section{Experimental Results} \label{resn-expr-sec}
-
-% use Jenkins daily build logs to rebuild speedup graph with more data
-
-% look back at Resolution Algorithms section for threads to tie up "does the algorithm look like this?"
-
 \section{Conclusion \& Future Work}