diff --git a/StatefulFW/StatefulCore.thy b/StatefulFW/StatefulCore.thy
index b92a676..384fe76 100644
--- a/StatefulFW/StatefulCore.thy
+++ b/StatefulFW/StatefulCore.thy
@@ -35,7 +35,7 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  *****************************************************************************)
 
-section {* Stateful Protocols *}
+subsection {* Stateful Protocols: Foundations *}
 theory 
   StatefulCore 
   imports 
@@ -103,4 +103,4 @@ fun ids where
 definition applyPolicy::  "('i \<times> ('i \<mapsto> 'o)) \<mapsto> 'o" 
   where     "applyPolicy = (\<lambda> (x,z). z x)"  
 
-end
\ No newline at end of file
+end
diff --git a/StatefulFW/StatefulFW.thy b/StatefulFW/StatefulFW.thy
index 9aaf7e4..9596bac 100644
--- a/StatefulFW/StatefulFW.thy
+++ b/StatefulFW/StatefulFW.thy
@@ -35,10 +35,10 @@
  * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
  *****************************************************************************)
 
-subsection {* Stateful Network Protocols *}
+section {* Stateful Network Protocols *}
 theory 
   StatefulFW
   imports
     FTPVOIP
 begin
-end
\ No newline at end of file
+end
diff --git a/document/root.tex b/document/root.tex
index 27fbd0b..7e19ba1 100644
--- a/document/root.tex
+++ b/document/root.tex
@@ -120,7 +120,8 @@
       \input{NormalisationGenericProofs.tex}
       \input{NormalisationIntegerPortProof.tex}
       \input{NormalisationIPPProofs.tex}
-    \input{Stateful}
+    \input{StatefulFW}
+      \input{StatefulCore}
       \input{FTP}
       \input{FTP_WithPolicy}
       \input{VOIP}