diff --git a/lean/Spa/Interp.lean b/lean/Spa/Interp.lean
index 62fb922..0123189 100644
--- a/lean/Spa/Interp.lean
+++ b/lean/Spa/Interp.lean
@@ -2,7 +2,7 @@ import Mathlib.Tactic.TypeStar
 
 /-!
 
-Interpretation to a semantic domain.
+# Interpretation to a Semantic Domain
 
 This file serves to introduce the double-angle-bracket "denotation"
 notation by prodiving a class instance `Interp`, whose single
diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean
index 5fcdc72..8038004 100644
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -2,7 +2,7 @@ import Mathlib.Data.Finset.Basic
 
 /-!
 
-Base language.
+# Base Language
 
 This file defines the core object language for the program analysis and
 transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean`
diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean
index e10c535..59c5223 100644
--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -5,7 +5,7 @@ import Mathlib.Data.List.FinRange
 
 /-!
 
-Algebraic Control Flow Graphs.
+# Algebraic Control Flow Graphs
 
 This file defines control flow graphs and operations to naturally compose them,
 making it possible to inductively covnert a program in the object language
diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean
index 5c59215..34cf3d7 100644
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -3,7 +3,7 @@ import Mathlib.Order.RelSeries
 
 /-!
 
-Lattice Definitions.
+# Lattice Definitions
 
 This file provides some definitions for lattices. It used to be more critical
 when this was an Agda project, since it defined (semi)lattices, the ordering