Changes

Summary

update Iptables_Semantics and friends: add multiport matches, output interface rewriting, reverse path filtering, etc.

Changeset 7396:134f9eb16d6f by michaelis: update Iptables_Semantics and friends: add multiport matches, output interface rewriting, reverse path filtering, etc.
The file was added	`thys/IP_Addresses/Prefix_Match_toString.thy`
The file was added	`thys/Iptables_Semantics/Primitive_Matchers/Output_Interface_Replace.thy`
The file was added	`thys/Routing/ReversePathFiltering.thy`
The file was added	`thys/Routing/ip-6-route-ex`
The file was modified	`thys/IP_Addresses/Prefix_Match.thy` (diff)
The file was modified	`thys/IP_Addresses/WordInterval.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Code_haskell.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Contrived/Contrived_Example.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/IPPartEval/IP_Address_Space_Examples_All_Small.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Parser_Test/Parser_Test.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Parser_Test/data/iptables-save` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Syntax.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_toString.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Interface_Replace.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Parser.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Routing_IpAssmt.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Transform.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/MatchExpr_Fold.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Negation_Type_Matching.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Normalized_Matches.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Simple_Firewall/SimpleFw_Compliance.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Documentation.thy` (diff)
The file was modified	`thys/Routing/IpRoute_Parser.ml` (diff)
The file was modified	`thys/Routing/IpRoute_Parser.thy` (diff)
The file was modified	`thys/Routing/Linorder_Helper.thy` (diff)
The file was modified	`thys/Routing/Routing_Table.thy` (diff)