diff --git a/thys/Iptables_Semantics/ROOT b/thys/Iptables_Semantics/ROOT
--- a/thys/Iptables_Semantics/ROOT
+++ b/thys/Iptables_Semantics/ROOT
@@ -1,95 +1,93 @@
 chapter AFP
 
 session Iptables_Semantics (AFP) = Routing +
   options [timeout = 1200]
   sessions
     Native_Word
   directories
     "Common"
     "Semantics_Ternary"
     "Primitive_Matchers"
     "Simple_Firewall"
   theories [document = false]
     "Common/List_Misc"
     "Common/WordInterval_Lists"
   theories
     Semantics
     Example_Semantics
     Alternative_Semantics
     Semantics_Stateful
     Semantics_Goto
     Call_Return_Unfolding
     "Common/Negation_Type_DNF"
     "Semantics_Ternary/Semantics_Ternary"
     Matching_Embeddings
     Semantics_Embeddings
     Iptables_Semantics
     Semantics_Stateful
     "Semantics_Ternary/Optimizing"
     "Primitive_Matchers/No_Spoof"
     "Primitive_Matchers/Parser6"
     No_Spoof_Embeddings
     "Primitive_Matchers/Routing_IpAssmt"
     "Primitive_Matchers/Transform"
     "Primitive_Matchers/Primitive_Abstract"
     "Primitive_Matchers/Code_Interface"
     "Primitive_Matchers/Parser"
     "Simple_Firewall/SimpleFw_Compliance"
     Code_haskell
     Access_Matrix_Embeddings
     No_Spoof_Embeddings
     Documentation
   document_files
     "root.tex"
     "root.bib"
     "mathpartir.sty"
 
 session Iptables_Semantics_Examples (AFP) in "Examples" = Iptables_Semantics +
   options [timeout = 2400]
   directories
     "Parser_Test"
     "Fail"
     "Contrived"
     "Synology_Diskstation_DS414"
     "Ringofsaturn_com"
     "SQRL_Shorewall"
     "sns.ias.edu"
     "medium-sized-company"
   theories
     "Parser_Test/Parser_Test"
     "Parser_Test/Parser6_Test"
     "Small_Examples"
     "Fail/Ports_Fail"
     "Contrived/Contrived_Example"
     "Synology_Diskstation_DS414/Analyze_Synology_Diskstation"
     "Ringofsaturn_com/Analyze_Ringofsaturn_com"
     "SQRL_Shorewall/Analyze_SQRL_Shorewall"
     "SQRL_Shorewall/SQRL_2015_nospoof"
     "sns.ias.edu/SNS_IAS_Eduroam_Spoofing"
     "medium-sized-company/Analyze_medium_sized_company"
   document_files (in "../document")
     "root.tex"
     "root.bib"
     "mathpartir.sty"
 
 session Iptables_Semantics_Examples_Big (AFP slow very_slow) in "Examples_Big" = Iptables_Semantics_Examples +
   options [timeout = 60000]
   directories
-    "../Examples/topoS_generated"
     "../Examples/IPPartEval"
     "../Examples/TUM_Net_Firewall"
     "../Examples/containern"
-    "../Examples/TUM_Net_Firewall"
-    "../Examples/IPPartEval"
+    "../Examples/topoS_generated"
   theories
     "../Examples/topoS_generated/Analyze_topos_generated"
     "../Examples/IPPartEval/IP_Address_Space_Examples_All_Small"
     "../Examples/TUM_Net_Firewall/Analyze_TUM_Net_Firewall"
     "../Examples/containern/Analyze_Containern"
     "../Examples/TUM_Net_Firewall/TUM_Spoofing_new3"
     "../Examples/TUM_Net_Firewall/TUM_Simple_FW"
     "../Examples/IPPartEval/IP_Address_Space_Examples_All_Large"
   document_files (in "../document")
     "root.tex"
     "root.bib"
     "mathpartir.sty"