From dcc46bdad04a798d09cde7eecbba2d01d29a4bea Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Mon, 2 Jan 2017 13:16:48 +0000
Subject: [PATCH] Fixed theory hierachy and includes.

---
 StatefulFW/StatefulCore.thy | 4 ++--
 StatefulFW/StatefulFW.thy   | 4 ++--
 document/root.tex           | 3 ++-
 3 files changed, 6 insertions(+), 5 deletions(-)

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}