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

Import of current (Isabelle 2017) release of UPF_Firewall.

This commit is contained in:
Achim D. Brucker 2017-12-02 22:30:05 +00:00
parent 494cd44eaf
commit 56bee1c2c4
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy
View File

@ -78,7 +78,7 @@ lemma aux0_6: "\<lbrakk>singleCombinators xs; \<not> (\<exists> a b. x = a \<opl
singleCombinators(x#xs)"
apply (rule aux0_1,simp_all)
apply (case_tac "x",simp_all)
by auto
done
lemma aux0_5: " \<not> (\<exists> a b. (a\<oplus>b) \<in> set x) \<Longrightarrow> singleCombinators x"
apply (induct "x")

2
UPF_Firewall/PacketFilter/PolicyCore.thy
View File

@ -40,7 +40,7 @@ theory
PolicyCore
imports
NetworkCore
"../../UPF/UPF"
UPF.UPF
begin