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