Updated setup to match AFP in-situ setup.

PacketFilter/PolicyCore.thy

@@ -38,8 +38,9 @@
 subsection {* Policy Core *}
 theory 
   PolicyCore
-  imports NetworkCore 
-    "$AFP/UPF/UPF"
+  imports 
+     NetworkCore 
+     "../../UPF/UPF"
 begin
 
 

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
 ```

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