From 17e0bd6e7e0c3727ca518e1e103e006f3425f849 Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Thu, 5 Jan 2017 13:40:37 +0000
Subject: [PATCH] Updated setup to match AFP in-situ setup.

---
 PacketFilter/PolicyCore.thy | 5 +++--
 README.md                   | 3 +++
 ROOT                        | 4 +---
 3 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/PacketFilter/PolicyCore.thy b/PacketFilter/PolicyCore.thy
index e1f4fae..cd66591 100644
--- a/PacketFilter/PolicyCore.thy
+++ b/PacketFilter/PolicyCore.thy
@@ -38,8 +38,9 @@
 subsection {* Policy Core *}
 theory 
   PolicyCore
-  imports NetworkCore 
-    "$AFP/UPF/UPF"
+  imports 
+     NetworkCore 
+     "../../UPF/UPF"
 begin
 
 
diff --git a/README.md b/README.md
index 5cde0e7..b4d9332 100644
--- a/README.md
+++ b/README.md
@@ -18,6 +18,9 @@ mkdir -p ~/.isabelle/Isabelle2016-1/etc
 echo "/home/isabelle/afp" >> ~/.isabelle/Isabelle2016-1/etc/components
 ```
 
+Now, you can either link the UPF entry to a sibling directory of UPF-Firewall such 
+that the import `../../UPF/UPF` in `PacketFilter/PolicyCore.thy` is valid. Alternatively, 
+you need to change this import to `$AFP/UPF/UPF`.
 
 ## How to build
 ```
diff --git a/ROOT b/ROOT
index 1eea235..4dc6ffa 100644
--- a/ROOT
+++ b/ROOT
@@ -1,6 +1,4 @@
-chapter AFP
-
-session "UPF-Firewall" (AFP) = HOL +
+session "UPF-Firewall" (AFP) = UPF +
   description {* Formal Network Models and Their Application to Firewall Policies *}
   options [timeout=600, document=pdf, document_output=document_generated, document_variants="document:outline=/proof,/ML"]
   theories