afp-mirror
/
UPF_Firewall
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fixed theory hierachy and includes.

This commit is contained in:
Achim D. Brucker 2017-01-02 13:16:48 +00:00
parent 17f828902e
commit dcc46bdad0
3 changed files with 6 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
StatefulFW/StatefulCore.thy
View File

@ -35,7 +35,7 @@
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*****************************************************************************) *****************************************************************************)
section {* Stateful Protocols *} subsection {* Stateful Protocols: Foundations *}
theory theory
StatefulCore StatefulCore
imports imports
@ -103,4 +103,4 @@ fun ids where
definition applyPolicy:: "('i \<times> ('i \<mapsto> 'o)) \<mapsto> 'o" definition applyPolicy:: "('i \<times> ('i \<mapsto> 'o)) \<mapsto> 'o"
where "applyPolicy = (\<lambda> (x,z). z x)" where "applyPolicy = (\<lambda> (x,z). z x)"
end end

4
StatefulFW/StatefulFW.thy
View File

@ -35,10 +35,10 @@
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*****************************************************************************) *****************************************************************************)
subsection {* Stateful Network Protocols *} section {* Stateful Network Protocols *}
theory theory
StatefulFW StatefulFW
imports imports
FTPVOIP FTPVOIP
begin begin
end end

3
document/root.tex
View File

@ -120,7 +120,8 @@
\input{NormalisationGenericProofs.tex} \input{NormalisationGenericProofs.tex}
\input{NormalisationIntegerPortProof.tex} \input{NormalisationIntegerPortProof.tex}
\input{NormalisationIPPProofs.tex} \input{NormalisationIPPProofs.tex}
\input{Stateful} \input{StatefulFW}
\input{StatefulCore}
\input{FTP} \input{FTP}
\input{FTP_WithPolicy} \input{FTP_WithPolicy}
\input{VOIP} \input{VOIP}