From da2138aa5990346c30a8a8dc85a78f4d9eb541b8 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 7 Jan 2017 20:42:39 +0000 Subject: [PATCH] Restructured file layout to match afp default. --- README.md | 2 +- {Examples => UPF-Firewall/Examples}/DMZ/DMZ.thy | 0 {Examples => UPF-Firewall/Examples}/DMZ/DMZDatatype.thy | 0 {Examples => UPF-Firewall/Examples}/DMZ/DMZInteger.thy | 0 {Examples => UPF-Firewall/Examples}/Examples.thy | 0 {Examples => UPF-Firewall/Examples}/NAT-FW/NAT-FW.thy | 0 .../Examples}/PersonalFirewall/PersonalFirewall.thy | 0 .../Examples}/PersonalFirewall/PersonalFirewallDatatype.thy | 0 .../Examples}/PersonalFirewall/PersonalFirewallInt.thy | 0 .../Examples}/PersonalFirewall/PersonalFirewallIpv4.thy | 0 .../Examples}/Transformation/Transformation.thy | 0 .../Examples}/Transformation/Transformation01.thy | 0 .../Examples}/Transformation/Transformation02.thy | 0 {Examples => UPF-Firewall/Examples}/VoIP/VoIP.thy | 0 .../FWNormalisation}/ElementaryRules.thy | 0 .../FWNormalisation}/FWNormalisation.thy | 0 .../FWNormalisation}/FWNormalisationCore.thy | 0 .../FWNormalisation}/NormalisationGenericProofs.thy | 0 .../FWNormalisation}/NormalisationIPPProofs.thy | 0 .../FWNormalisation}/NormalisationIntegerPortProof.thy | 0 {NAT => UPF-Firewall/NAT}/NAT.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/DatatypeAddress.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/DatatypePort.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/IPv4.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/IPv4_TCPUDP.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/IntegerAddress.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/IntegerPort.thy | 0 .../PacketFilter}/IntegerPort_TCPUDP.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/NetworkCore.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/NetworkModels.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/PacketFilter.thy | 0 .../PacketFilter}/PolicyCombinators.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/PolicyCore.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/PortCombinators.thy | 0 {PacketFilter => UPF-Firewall/PacketFilter}/Ports.thy | 0 .../PacketFilter}/ProtocolPortCombinators.thy | 0 ROOT => UPF-Firewall/ROOT | 0 {StatefulFW => UPF-Firewall/StatefulFW}/FTP.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/FTPVOIP.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/FTP_WithPolicy.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/LTL_alike.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/StatefulCore.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/StatefulFW.thy | 0 {StatefulFW => UPF-Firewall/StatefulFW}/VOIP.thy | 0 UPF-Firewall.thy => UPF-Firewall/UPF-Firewall.thy | 0 {document => UPF-Firewall/document}/introduction.tex | 0 {document => UPF-Firewall/document}/root.bib | 0 {document => UPF-Firewall/document}/root.tex | 0 48 files changed, 1 insertion(+), 1 deletion(-) rename {Examples => UPF-Firewall/Examples}/DMZ/DMZ.thy (100%) rename {Examples => UPF-Firewall/Examples}/DMZ/DMZDatatype.thy (100%) rename {Examples => UPF-Firewall/Examples}/DMZ/DMZInteger.thy (100%) rename {Examples => UPF-Firewall/Examples}/Examples.thy (100%) rename {Examples => UPF-Firewall/Examples}/NAT-FW/NAT-FW.thy (100%) rename {Examples => UPF-Firewall/Examples}/PersonalFirewall/PersonalFirewall.thy (100%) rename {Examples => UPF-Firewall/Examples}/PersonalFirewall/PersonalFirewallDatatype.thy (100%) rename {Examples => UPF-Firewall/Examples}/PersonalFirewall/PersonalFirewallInt.thy (100%) rename {Examples => UPF-Firewall/Examples}/PersonalFirewall/PersonalFirewallIpv4.thy (100%) rename {Examples => UPF-Firewall/Examples}/Transformation/Transformation.thy (100%) rename {Examples => UPF-Firewall/Examples}/Transformation/Transformation01.thy (100%) rename {Examples => UPF-Firewall/Examples}/Transformation/Transformation02.thy (100%) rename {Examples => UPF-Firewall/Examples}/VoIP/VoIP.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/ElementaryRules.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/FWNormalisation.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/FWNormalisationCore.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/NormalisationGenericProofs.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/NormalisationIPPProofs.thy (100%) rename {FWNormalisation => UPF-Firewall/FWNormalisation}/NormalisationIntegerPortProof.thy (100%) rename {NAT => UPF-Firewall/NAT}/NAT.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/DatatypeAddress.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/DatatypePort.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/IPv4.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/IPv4_TCPUDP.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/IntegerAddress.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/IntegerPort.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/IntegerPort_TCPUDP.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/NetworkCore.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/NetworkModels.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/PacketFilter.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/PolicyCombinators.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/PolicyCore.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/PortCombinators.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/Ports.thy (100%) rename {PacketFilter => UPF-Firewall/PacketFilter}/ProtocolPortCombinators.thy (100%) rename ROOT => UPF-Firewall/ROOT (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/FTP.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/FTPVOIP.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/FTP_WithPolicy.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/LTL_alike.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/StatefulCore.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/StatefulFW.thy (100%) rename {StatefulFW => UPF-Firewall/StatefulFW}/VOIP.thy (100%) rename UPF-Firewall.thy => UPF-Firewall/UPF-Firewall.thy (100%) rename {document => UPF-Firewall/document}/introduction.tex (100%) rename {document => UPF-Firewall/document}/root.bib (100%) rename {document => UPF-Firewall/document}/root.tex (100%) diff --git a/README.md b/README.md index b4d9332..5b32eab 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ you need to change this import to `$AFP/UPF/UPF`. ## How to build ``` -isabelle build -d . UPF-Firewall +isabelle build -d UPF-Firewall . UPF-Firewall ``` ## Authors diff --git a/Examples/DMZ/DMZ.thy b/UPF-Firewall/Examples/DMZ/DMZ.thy similarity index 100% rename from Examples/DMZ/DMZ.thy rename to UPF-Firewall/Examples/DMZ/DMZ.thy diff --git a/Examples/DMZ/DMZDatatype.thy b/UPF-Firewall/Examples/DMZ/DMZDatatype.thy similarity index 100% rename from Examples/DMZ/DMZDatatype.thy rename to UPF-Firewall/Examples/DMZ/DMZDatatype.thy diff --git a/Examples/DMZ/DMZInteger.thy b/UPF-Firewall/Examples/DMZ/DMZInteger.thy similarity index 100% rename from Examples/DMZ/DMZInteger.thy rename to UPF-Firewall/Examples/DMZ/DMZInteger.thy diff --git a/Examples/Examples.thy b/UPF-Firewall/Examples/Examples.thy similarity index 100% rename from Examples/Examples.thy rename to UPF-Firewall/Examples/Examples.thy diff --git a/Examples/NAT-FW/NAT-FW.thy b/UPF-Firewall/Examples/NAT-FW/NAT-FW.thy similarity index 100% rename from Examples/NAT-FW/NAT-FW.thy rename to UPF-Firewall/Examples/NAT-FW/NAT-FW.thy diff --git a/Examples/PersonalFirewall/PersonalFirewall.thy b/UPF-Firewall/Examples/PersonalFirewall/PersonalFirewall.thy similarity index 100% rename from Examples/PersonalFirewall/PersonalFirewall.thy rename to UPF-Firewall/Examples/PersonalFirewall/PersonalFirewall.thy diff --git a/Examples/PersonalFirewall/PersonalFirewallDatatype.thy b/UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy similarity index 100% rename from Examples/PersonalFirewall/PersonalFirewallDatatype.thy rename to UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy diff --git a/Examples/PersonalFirewall/PersonalFirewallInt.thy b/UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy similarity index 100% rename from Examples/PersonalFirewall/PersonalFirewallInt.thy rename to UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy diff --git a/Examples/PersonalFirewall/PersonalFirewallIpv4.thy b/UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy similarity index 100% rename from Examples/PersonalFirewall/PersonalFirewallIpv4.thy rename to UPF-Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy diff --git a/Examples/Transformation/Transformation.thy b/UPF-Firewall/Examples/Transformation/Transformation.thy similarity index 100% rename from Examples/Transformation/Transformation.thy rename to UPF-Firewall/Examples/Transformation/Transformation.thy diff --git a/Examples/Transformation/Transformation01.thy b/UPF-Firewall/Examples/Transformation/Transformation01.thy similarity index 100% rename from Examples/Transformation/Transformation01.thy rename to UPF-Firewall/Examples/Transformation/Transformation01.thy diff --git a/Examples/Transformation/Transformation02.thy b/UPF-Firewall/Examples/Transformation/Transformation02.thy similarity index 100% rename from Examples/Transformation/Transformation02.thy rename to UPF-Firewall/Examples/Transformation/Transformation02.thy diff --git a/Examples/VoIP/VoIP.thy b/UPF-Firewall/Examples/VoIP/VoIP.thy similarity index 100% rename from Examples/VoIP/VoIP.thy rename to UPF-Firewall/Examples/VoIP/VoIP.thy diff --git a/FWNormalisation/ElementaryRules.thy b/UPF-Firewall/FWNormalisation/ElementaryRules.thy similarity index 100% rename from FWNormalisation/ElementaryRules.thy rename to UPF-Firewall/FWNormalisation/ElementaryRules.thy diff --git a/FWNormalisation/FWNormalisation.thy b/UPF-Firewall/FWNormalisation/FWNormalisation.thy similarity index 100% rename from FWNormalisation/FWNormalisation.thy rename to UPF-Firewall/FWNormalisation/FWNormalisation.thy diff --git a/FWNormalisation/FWNormalisationCore.thy b/UPF-Firewall/FWNormalisation/FWNormalisationCore.thy similarity index 100% rename from FWNormalisation/FWNormalisationCore.thy rename to UPF-Firewall/FWNormalisation/FWNormalisationCore.thy diff --git a/FWNormalisation/NormalisationGenericProofs.thy b/UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy similarity index 100% rename from FWNormalisation/NormalisationGenericProofs.thy rename to UPF-Firewall/FWNormalisation/NormalisationGenericProofs.thy diff --git a/FWNormalisation/NormalisationIPPProofs.thy b/UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy similarity index 100% rename from FWNormalisation/NormalisationIPPProofs.thy rename to UPF-Firewall/FWNormalisation/NormalisationIPPProofs.thy diff --git a/FWNormalisation/NormalisationIntegerPortProof.thy b/UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy similarity index 100% rename from FWNormalisation/NormalisationIntegerPortProof.thy rename to UPF-Firewall/FWNormalisation/NormalisationIntegerPortProof.thy diff --git a/NAT/NAT.thy b/UPF-Firewall/NAT/NAT.thy similarity index 100% rename from NAT/NAT.thy rename to UPF-Firewall/NAT/NAT.thy diff --git a/PacketFilter/DatatypeAddress.thy b/UPF-Firewall/PacketFilter/DatatypeAddress.thy similarity index 100% rename from PacketFilter/DatatypeAddress.thy rename to UPF-Firewall/PacketFilter/DatatypeAddress.thy diff --git a/PacketFilter/DatatypePort.thy b/UPF-Firewall/PacketFilter/DatatypePort.thy similarity index 100% rename from PacketFilter/DatatypePort.thy rename to UPF-Firewall/PacketFilter/DatatypePort.thy diff --git a/PacketFilter/IPv4.thy b/UPF-Firewall/PacketFilter/IPv4.thy similarity index 100% rename from PacketFilter/IPv4.thy rename to UPF-Firewall/PacketFilter/IPv4.thy diff --git a/PacketFilter/IPv4_TCPUDP.thy b/UPF-Firewall/PacketFilter/IPv4_TCPUDP.thy similarity index 100% rename from PacketFilter/IPv4_TCPUDP.thy rename to UPF-Firewall/PacketFilter/IPv4_TCPUDP.thy diff --git a/PacketFilter/IntegerAddress.thy b/UPF-Firewall/PacketFilter/IntegerAddress.thy similarity index 100% rename from PacketFilter/IntegerAddress.thy rename to UPF-Firewall/PacketFilter/IntegerAddress.thy diff --git a/PacketFilter/IntegerPort.thy b/UPF-Firewall/PacketFilter/IntegerPort.thy similarity index 100% rename from PacketFilter/IntegerPort.thy rename to UPF-Firewall/PacketFilter/IntegerPort.thy diff --git a/PacketFilter/IntegerPort_TCPUDP.thy b/UPF-Firewall/PacketFilter/IntegerPort_TCPUDP.thy similarity index 100% rename from PacketFilter/IntegerPort_TCPUDP.thy rename to UPF-Firewall/PacketFilter/IntegerPort_TCPUDP.thy diff --git a/PacketFilter/NetworkCore.thy b/UPF-Firewall/PacketFilter/NetworkCore.thy similarity index 100% rename from PacketFilter/NetworkCore.thy rename to UPF-Firewall/PacketFilter/NetworkCore.thy diff --git a/PacketFilter/NetworkModels.thy b/UPF-Firewall/PacketFilter/NetworkModels.thy similarity index 100% rename from PacketFilter/NetworkModels.thy rename to UPF-Firewall/PacketFilter/NetworkModels.thy diff --git a/PacketFilter/PacketFilter.thy b/UPF-Firewall/PacketFilter/PacketFilter.thy similarity index 100% rename from PacketFilter/PacketFilter.thy rename to UPF-Firewall/PacketFilter/PacketFilter.thy diff --git a/PacketFilter/PolicyCombinators.thy b/UPF-Firewall/PacketFilter/PolicyCombinators.thy similarity index 100% rename from PacketFilter/PolicyCombinators.thy rename to UPF-Firewall/PacketFilter/PolicyCombinators.thy diff --git a/PacketFilter/PolicyCore.thy b/UPF-Firewall/PacketFilter/PolicyCore.thy similarity index 100% rename from PacketFilter/PolicyCore.thy rename to UPF-Firewall/PacketFilter/PolicyCore.thy diff --git a/PacketFilter/PortCombinators.thy b/UPF-Firewall/PacketFilter/PortCombinators.thy similarity index 100% rename from PacketFilter/PortCombinators.thy rename to UPF-Firewall/PacketFilter/PortCombinators.thy diff --git a/PacketFilter/Ports.thy b/UPF-Firewall/PacketFilter/Ports.thy similarity index 100% rename from PacketFilter/Ports.thy rename to UPF-Firewall/PacketFilter/Ports.thy diff --git a/PacketFilter/ProtocolPortCombinators.thy b/UPF-Firewall/PacketFilter/ProtocolPortCombinators.thy similarity index 100% rename from PacketFilter/ProtocolPortCombinators.thy rename to UPF-Firewall/PacketFilter/ProtocolPortCombinators.thy diff --git a/ROOT b/UPF-Firewall/ROOT similarity index 100% rename from ROOT rename to UPF-Firewall/ROOT diff --git a/StatefulFW/FTP.thy b/UPF-Firewall/StatefulFW/FTP.thy similarity index 100% rename from StatefulFW/FTP.thy rename to UPF-Firewall/StatefulFW/FTP.thy diff --git a/StatefulFW/FTPVOIP.thy b/UPF-Firewall/StatefulFW/FTPVOIP.thy similarity index 100% rename from StatefulFW/FTPVOIP.thy rename to UPF-Firewall/StatefulFW/FTPVOIP.thy diff --git a/StatefulFW/FTP_WithPolicy.thy b/UPF-Firewall/StatefulFW/FTP_WithPolicy.thy similarity index 100% rename from StatefulFW/FTP_WithPolicy.thy rename to UPF-Firewall/StatefulFW/FTP_WithPolicy.thy diff --git a/StatefulFW/LTL_alike.thy b/UPF-Firewall/StatefulFW/LTL_alike.thy similarity index 100% rename from StatefulFW/LTL_alike.thy rename to UPF-Firewall/StatefulFW/LTL_alike.thy diff --git a/StatefulFW/StatefulCore.thy b/UPF-Firewall/StatefulFW/StatefulCore.thy similarity index 100% rename from StatefulFW/StatefulCore.thy rename to UPF-Firewall/StatefulFW/StatefulCore.thy diff --git a/StatefulFW/StatefulFW.thy b/UPF-Firewall/StatefulFW/StatefulFW.thy similarity index 100% rename from StatefulFW/StatefulFW.thy rename to UPF-Firewall/StatefulFW/StatefulFW.thy diff --git a/StatefulFW/VOIP.thy b/UPF-Firewall/StatefulFW/VOIP.thy similarity index 100% rename from StatefulFW/VOIP.thy rename to UPF-Firewall/StatefulFW/VOIP.thy diff --git a/UPF-Firewall.thy b/UPF-Firewall/UPF-Firewall.thy similarity index 100% rename from UPF-Firewall.thy rename to UPF-Firewall/UPF-Firewall.thy diff --git a/document/introduction.tex b/UPF-Firewall/document/introduction.tex similarity index 100% rename from document/introduction.tex rename to UPF-Firewall/document/introduction.tex diff --git a/document/root.bib b/UPF-Firewall/document/root.bib similarity index 100% rename from document/root.bib rename to UPF-Firewall/document/root.bib diff --git a/document/root.tex b/UPF-Firewall/document/root.tex similarity index 100% rename from document/root.tex rename to UPF-Firewall/document/root.tex