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

Migration to Isabelle 2021-1 (based on afp-2021-12-28).

This commit is contained in:
Achim D. Brucker 2021-12-28 09:00:23 +00:00
parent b8df20bd53
commit 730226750e
3 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
View File

@ -1214,7 +1214,7 @@ next
case (3 v va vb y z) thus ?case
apply (cases "z = []", simp_all)
apply (simp add: PLemmas(8) UPFDefs(8) list2FWpolicyconc sepnMT)
by (metis (no_types, hide_lams) Conc_not_MT Cdom2 nlpaux domIff l2p_aux sepnMT)
by (metis (no_types, opaque_lifting) Conc_not_MT Cdom2 nlpaux domIff l2p_aux sepnMT)
next
case (4 v va y z) thus ?case
apply (cases "z = []", simp_all)

2
UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
View File

@ -470,7 +470,7 @@ next
apply (case_tac "xs = []", simp_all)
unfolding removeShadowRules1_alternative_def
apply (case_tac x, simp_all)
by (metis (no_types, hide_lams) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114
by (metis (no_types, opaque_lifting) CConcEnd2 CConcStart C_DenyAll RS1n_nMT aux114
domIff removeShadowRules1_alternative_def
removeShadowRules1_alternative_rev.simps(2) rev.simps(2))
done

1
UPF_Firewall/document/root.tex
View File

@ -1,4 +1,5 @@
\documentclass[11pt,DIV10,a4paper,twoside=semi,openright,titlepage]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm