new directory structure

diekmann · Dec 4, 2015 · 0826823 · 0826823
1 parent 84221cf
commit 0826823
Show file tree

Hide file tree

Showing 172 changed files with 4 additions and 3 deletions.
diff --git a/.gitmodules b/.gitmodules
@@ -1,3 +1,3 @@
-[submodule "Bitmagic/l4v"]
+[submodule "thy/Bitmagic/l4v"]
-	path = Bitmagic/l4v
+	path = thy/Bitmagic/l4v
 	url = https://github.com/seL4/l4v.git
diff --git a/ROOTS b/ROOTS
@@ -1 +1 @@
-Bitmagic
+thy
diff --git a/Attic.thy → thy/Attic.thy b/Attic.thy → thy/Attic.thy
diff --git a/Bitmagic/CIDRSplit.thy → thy/Bitmagic/CIDRSplit.thy b/Bitmagic/CIDRSplit.thy → thy/Bitmagic/CIDRSplit.thy
diff --git a/Bitmagic/IPv4Addr.thy → thy/Bitmagic/IPv4Addr.thy b/Bitmagic/IPv4Addr.thy → thy/Bitmagic/IPv4Addr.thy
diff --git a/Bitmagic/NumberWang.thy → thy/Bitmagic/NumberWang.thy b/Bitmagic/NumberWang.thy → thy/Bitmagic/NumberWang.thy
diff --git a/Bitmagic/NumberWangCaesar.thy → thy/Bitmagic/NumberWangCaesar.thy b/Bitmagic/NumberWangCaesar.thy → thy/Bitmagic/NumberWangCaesar.thy
diff --git a/Bitmagic/NumberWangCebewee.thy → thy/Bitmagic/NumberWangCebewee.thy b/Bitmagic/NumberWangCebewee.thy → thy/Bitmagic/NumberWangCebewee.thy
diff --git a/Bitmagic/Numberwang_Ln.thy → thy/Bitmagic/Numberwang_Ln.thy b/Bitmagic/Numberwang_Ln.thy → thy/Bitmagic/Numberwang_Ln.thy
diff --git a/Bitmagic/ROOT → thy/Bitmagic/ROOT b/Bitmagic/ROOT → thy/Bitmagic/ROOT
diff --git a/Bitmagic/WordInterval.thy → thy/Bitmagic/WordInterval.thy b/Bitmagic/WordInterval.thy → thy/Bitmagic/WordInterval.thy
diff --git a/Bitmagic/WordInterval_Lists.thy → thy/Bitmagic/WordInterval_Lists.thy b/Bitmagic/WordInterval_Lists.thy → thy/Bitmagic/WordInterval_Lists.thy
diff --git a/Bitmagic/WordInterval_NumberWang.thy → thy/Bitmagic/WordInterval_NumberWang.thy b/Bitmagic/WordInterval_NumberWang.thy → thy/Bitmagic/WordInterval_NumberWang.thy
diff --git a/Bitmagic/Word_Next.thy → thy/Bitmagic/Word_Next.thy b/Bitmagic/Word_Next.thy → thy/Bitmagic/Word_Next.thy
diff --git a/Bitmagic/document/root.tex → thy/Bitmagic/document/root.tex b/Bitmagic/document/root.tex → thy/Bitmagic/document/root.tex
diff --git a/Bitmagic/l4v → thy/Bitmagic/l4v b/Bitmagic/l4v → thy/Bitmagic/l4v
diff --git a/Call_Return_Unfolding.thy → thy/Call_Return_Unfolding.thy b/Call_Return_Unfolding.thy → thy/Call_Return_Unfolding.thy
diff --git a/Common/Lib_toString.thy → thy/Common/Lib_toString.thy b/Common/Lib_toString.thy → thy/Common/Lib_toString.thy
diff --git a/Common/Negation_Type.thy → thy/Common/Negation_Type.thy b/Common/Negation_Type.thy → thy/Common/Negation_Type.thy
diff --git a/Common/Negation_Type_DNF.thy → thy/Common/Negation_Type_DNF.thy b/Common/Negation_Type_DNF.thy → thy/Common/Negation_Type_DNF.thy
diff --git a/Common/Remdups_Rev.thy → thy/Common/Remdups_Rev.thy b/Common/Remdups_Rev.thy → thy/Common/Remdups_Rev.thy
diff --git a/Common/SetPartitioning.thy → thy/Common/SetPartitioning.thy b/Common/SetPartitioning.thy → thy/Common/SetPartitioning.thy
diff --git a/Common/Ternary.thy → thy/Common/Ternary.thy b/Common/Ternary.thy → thy/Common/Ternary.thy
diff --git a/Datatype_Selectors.thy → thy/Datatype_Selectors.thy b/Datatype_Selectors.thy → thy/Datatype_Selectors.thy
diff --git a/Examples/Code_haskell.thy → thy/Examples/Code_haskell.thy b/Examples/Code_haskell.thy → thy/Examples/Code_haskell.thy
diff --git a/Examples/Example_Semantics.thy → thy/Examples/Example_Semantics.thy b/Examples/Example_Semantics.thy → thy/Examples/Example_Semantics.thy
diff --git a/...l/IP_Address_Space_Examples_All_Large.thy → ...l/IP_Address_Space_Examples_All_Large.thy b/...l/IP_Address_Space_Examples_All_Large.thy → ...l/IP_Address_Space_Examples_All_Large.thy
diff --git a/...l/IP_Address_Space_Examples_All_Small.thy → ...l/IP_Address_Space_Examples_All_Small.thy b/...l/IP_Address_Space_Examples_All_Small.thy → ...l/IP_Address_Space_Examples_All_Small.thy
diff --git a/...TUM_Net/iptables-save-2015-05-15_15-23-41 → ...TUM_Net/iptables-save-2015-05-15_15-23-41 b/...TUM_Net/iptables-save-2015-05-15_15-23-41 → ...TUM_Net/iptables-save-2015-05-15_15-23-41
diff --git a/...les-save-2015-05-15_15-23-41.Ln.FWD.lower → ...les-save-2015-05-15_15-23-41.Ln.FWD.lower b/...les-save-2015-05-15_15-23-41.Ln.FWD.lower → ...les-save-2015-05-15_15-23-41.Ln.FWD.lower
diff --git a/...les-save-2015-05-15_15-23-41.Ln.FWD.upper → ...les-save-2015-05-15_15-23-41.Ln.FWD.upper b/...les-save-2015-05-15_15-23-41.Ln.FWD.upper → ...les-save-2015-05-15_15-23-41.Ln.FWD.upper
diff --git a/...TUM_Net/iptables-save-2015-09-03_15-56-50 → ...TUM_Net/iptables-save-2015-09-03_15-56-50 b/...TUM_Net/iptables-save-2015-09-03_15-56-50 → ...TUM_Net/iptables-save-2015-09-03_15-56-50
diff --git a/...les-save-2015-09-03_15-56-50.Ln.FWD.lower → ...les-save-2015-09-03_15-56-50.Ln.FWD.lower b/...les-save-2015-09-03_15-56-50.Ln.FWD.lower → ...les-save-2015-09-03_15-56-50.Ln.FWD.lower
diff --git a/...les-save-2015-09-03_15-56-50.Ln.FWD.upper → ...les-save-2015-09-03_15-56-50.Ln.FWD.upper b/...les-save-2015-09-03_15-56-50.Ln.FWD.upper → ...les-save-2015-09-03_15-56-50.Ln.FWD.upper
diff --git a/...es/IPPartEval/TUM_Net/iptables_20.10.2013 → ...es/IPPartEval/TUM_Net/iptables_20.10.2013 b/...es/IPPartEval/TUM_Net/iptables_20.10.2013 → ...es/IPPartEval/TUM_Net/iptables_20.10.2013
diff --git a/.../TUM_Net/iptables_20.10.2013.Ln.FWD.lower → .../TUM_Net/iptables_20.10.2013.Ln.FWD.lower b/.../TUM_Net/iptables_20.10.2013.Ln.FWD.lower → .../TUM_Net/iptables_20.10.2013.Ln.FWD.lower
diff --git a/.../TUM_Net/iptables_20.10.2013.Ln.FWD.upper → .../TUM_Net/iptables_20.10.2013.Ln.FWD.upper b/.../TUM_Net/iptables_20.10.2013.Ln.FWD.upper → .../TUM_Net/iptables_20.10.2013.Ln.FWD.upper
diff --git a/...es/IPPartEval/TUM_Net/iptables_25.07.2014 → ...es/IPPartEval/TUM_Net/iptables_25.07.2014 b/...es/IPPartEval/TUM_Net/iptables_25.07.2014 → ...es/IPPartEval/TUM_Net/iptables_25.07.2014
diff --git a/.../TUM_Net/iptables_25.07.2014.Ln.FWD.lower → .../TUM_Net/iptables_25.07.2014.Ln.FWD.lower b/.../TUM_Net/iptables_25.07.2014.Ln.FWD.lower → .../TUM_Net/iptables_25.07.2014.Ln.FWD.lower
diff --git a/.../TUM_Net/iptables_25.07.2014.Ln.FWD.upper → .../TUM_Net/iptables_25.07.2014.Ln.FWD.upper b/.../TUM_Net/iptables_25.07.2014.Ln.FWD.upper → .../TUM_Net/iptables_25.07.2014.Ln.FWD.upper
diff --git a/..._home_user/typical_home_user.Ln.FWD.lower → ..._home_user/typical_home_user.Ln.FWD.lower b/..._home_user/typical_home_user.Ln.FWD.lower → ..._home_user/typical_home_user.Ln.FWD.lower
diff --git a/..._home_user/typical_home_user.Ln.FWD.upper → ..._home_user/typical_home_user.Ln.FWD.upper b/..._home_user/typical_home_user.Ln.FWD.upper → ..._home_user/typical_home_user.Ln.FWD.upper
diff --git a/...home_user/typical_home_user_iptables-save → ...home_user/typical_home_user_iptables-save b/...home_user/typical_home_user_iptables-save → ...home_user/typical_home_user_iptables-save
diff --git a/...Eval/config_memphis_testbed/iptables-save → ...Eval/config_memphis_testbed/iptables-save b/...Eval/config_memphis_testbed/iptables-save → ...Eval/config_memphis_testbed/iptables-save
diff --git a/...fig_memphis_testbed/iptables.Ln.FWD.lower → ...fig_memphis_testbed/iptables.Ln.FWD.lower b/...fig_memphis_testbed/iptables.Ln.FWD.lower → ...fig_memphis_testbed/iptables.Ln.FWD.lower
diff --git a/...fig_memphis_testbed/iptables.Ln.FWD.upper → ...fig_memphis_testbed/iptables.Ln.FWD.upper b/...fig_memphis_testbed/iptables.Ln.FWD.upper → ...fig_memphis_testbed/iptables.Ln.FWD.upper
diff --git a/...PPartEval/config_random_srv/iptables-save → ...PPartEval/config_random_srv/iptables-save b/...PPartEval/config_random_srv/iptables-save → ...PPartEval/config_random_srv/iptables-save
diff --git a/...l/config_random_srv/iptables.INP.Ln.lower → ...l/config_random_srv/iptables.INP.Ln.lower b/...l/config_random_srv/iptables.INP.Ln.lower → ...l/config_random_srv/iptables.INP.Ln.lower
diff --git a/...l/config_random_srv/iptables.INP.Ln.upper → ...l/config_random_srv/iptables.INP.Ln.upper b/...l/config_random_srv/iptables.INP.Ln.upper → ...l/config_random_srv/iptables.INP.Ln.upper
diff --git a/...l_shorewall/2014_sep_iptables-saveakachan → ...l_shorewall/2014_sep_iptables-saveakachan b/...l_shorewall/2014_sep_iptables-saveakachan → ...l_shorewall/2014_sep_iptables-saveakachan
diff --git a/...014_sep_iptables-saveakachan.Ln.FWD.lower → ...014_sep_iptables-saveakachan.Ln.FWD.lower b/...014_sep_iptables-saveakachan.Ln.FWD.lower → ...014_sep_iptables-saveakachan.Ln.FWD.lower
diff --git a/...014_sep_iptables-saveakachan.Ln.FWD.upper → ...014_sep_iptables-saveakachan.Ln.FWD.upper b/...014_sep_iptables-saveakachan.Ln.FWD.upper → ...014_sep_iptables-saveakachan.Ln.FWD.upper
diff --git a/...015_aug_iptables-save-spoofing-protection → ...015_aug_iptables-save-spoofing-protection b/...015_aug_iptables-save-spoofing-protection → ...015_aug_iptables-save-spoofing-protection
diff --git a/...les-save-spoofing-protection.Ln.FWD.lower → ...les-save-spoofing-protection.Ln.FWD.lower b/...les-save-spoofing-protection.Ln.FWD.lower → ...les-save-spoofing-protection.Ln.FWD.lower
diff --git a/...les-save-spoofing-protection.Ln.FWD.upper → ...les-save-spoofing-protection.Ln.FWD.upper b/...les-save-spoofing-protection.Ln.FWD.upper → ...les-save-spoofing-protection.Ln.FWD.upper
diff --git a/...les-save-spoofing-protection.Ln.INP.lower → ...les-save-spoofing-protection.Ln.INP.lower b/...les-save-spoofing-protection.Ln.INP.lower → ...les-save-spoofing-protection.Ln.INP.lower
diff --git a/...les-save-spoofing-protection.Ln.INP.upper → ...les-save-spoofing-protection.Ln.INP.upper b/...les-save-spoofing-protection.Ln.INP.upper → ...les-save-spoofing-protection.Ln.INP.upper
diff --git a/...al/configs_srvs_ufw/server2-iptables-save → ...al/configs_srvs_ufw/server2-iptables-save b/...al/configs_srvs_ufw/server2-iptables-save → ...al/configs_srvs_ufw/server2-iptables-save
diff --git a/...vs_ufw/server2-iptables-save.Ln.INP.lower → ...vs_ufw/server2-iptables-save.Ln.INP.lower b/...vs_ufw/server2-iptables-save.Ln.INP.lower → ...vs_ufw/server2-iptables-save.Ln.INP.lower
diff --git a/...vs_ufw/server2-iptables-save.Ln.INP.upper → ...vs_ufw/server2-iptables-save.Ln.INP.upper b/...vs_ufw/server2-iptables-save.Ln.INP.upper → ...vs_ufw/server2-iptables-save.Ln.INP.upper
diff --git a/...4/iptables-save_jun_2015_legacyifacerules → ...4/iptables-save_jun_2015_legacyifacerules b/...4/iptables-save_jun_2015_legacyifacerules → ...4/iptables-save_jun_2015_legacyifacerules
diff --git a/...ve_jun_2015_legacyifacerules.Ln.INP.lower → ...ve_jun_2015_legacyifacerules.Ln.INP.lower b/...ve_jun_2015_legacyifacerules.Ln.INP.lower → ...ve_jun_2015_legacyifacerules.Ln.INP.lower
diff --git a/...ve_jun_2015_legacyifacerules.Ln.INP.upper → ...ve_jun_2015_legacyifacerules.Ln.INP.upper b/...ve_jun_2015_legacyifacerules.Ln.INP.upper → ...ve_jun_2015_legacyifacerules.Ln.INP.upper
diff --git a/...Eval/gopherproxy.meulie.net/iptables-save → ...Eval/gopherproxy.meulie.net/iptables-save b/...Eval/gopherproxy.meulie.net/iptables-save → ...Eval/gopherproxy.meulie.net/iptables-save
diff --git a/...oxy.meulie.net/iptables-save.Ln.INP.lower → ...oxy.meulie.net/iptables-save.Ln.INP.lower b/...oxy.meulie.net/iptables-save.Ln.INP.lower → ...oxy.meulie.net/iptables-save.Ln.INP.lower
diff --git a/...oxy.meulie.net/iptables-save.Ln.INP.upper → ...oxy.meulie.net/iptables-save.Ln.INP.upper b/...oxy.meulie.net/iptables-save.Ln.INP.upper → ...oxy.meulie.net/iptables-save.Ln.INP.upper
diff --git a/...IPPartEval/gopherproxy.meulie.net/results → ...IPPartEval/gopherproxy.meulie.net/results b/...IPPartEval/gopherproxy.meulie.net/results → ...IPPartEval/gopherproxy.meulie.net/results
diff --git a/Examples/IPPartEval/iptables_restore.sh → thy/Examples/IPPartEval/iptables_restore.sh b/Examples/IPPartEval/iptables_restore.sh → thy/Examples/IPPartEval/iptables_restore.sh
diff --git a/...les/IPPartEval/linux.gda.pl/firewallp.txt → ...les/IPPartEval/linux.gda.pl/firewallp.txt b/...les/IPPartEval/linux.gda.pl/firewallp.txt → ...les/IPPartEval/linux.gda.pl/firewallp.txt
diff --git a/...l/linux.gda.pl/firewallp.txt.Ln.FWD.lower → ...l/linux.gda.pl/firewallp.txt.Ln.FWD.lower b/...l/linux.gda.pl/firewallp.txt.Ln.FWD.lower → ...l/linux.gda.pl/firewallp.txt.Ln.FWD.lower
diff --git a/...l/linux.gda.pl/firewallp.txt.Ln.FWD.upper → ...l/linux.gda.pl/firewallp.txt.Ln.FWD.upper b/...l/linux.gda.pl/firewallp.txt.Ln.FWD.upper → ...l/linux.gda.pl/firewallp.txt.Ln.FWD.upper
diff --git a/Examples/IPPartEval/openvpn.eu/iptables-save → ...mples/IPPartEval/openvpn.eu/iptables-save b/Examples/IPPartEval/openvpn.eu/iptables-save → ...mples/IPPartEval/openvpn.eu/iptables-save
diff --git a/...val/openvpn.eu/iptables-save.Ln.FWD.lower → ...val/openvpn.eu/iptables-save.Ln.FWD.lower b/...val/openvpn.eu/iptables-save.Ln.FWD.lower → ...val/openvpn.eu/iptables-save.Ln.FWD.lower
diff --git a/...val/openvpn.eu/iptables-save.Ln.FWD.upper → ...val/openvpn.eu/iptables-save.Ln.FWD.upper b/...val/openvpn.eu/iptables-save.Ln.FWD.upper → ...val/openvpn.eu/iptables-save.Ln.FWD.upper
diff --git a/Examples/IPPartEval/openvpn.eu/src → thy/Examples/IPPartEval/openvpn.eu/src b/Examples/IPPartEval/openvpn.eu/src → thy/Examples/IPPartEval/openvpn.eu/src
diff --git a/...rt.org/iptables-save-AA.txt_fixed_newline → ...rt.org/iptables-save-AA.txt_fixed_newline b/...rt.org/iptables-save-AA.txt_fixed_newline → ...rt.org/iptables-save-AA.txt_fixed_newline
diff --git a/...es-save-AA.txt_fixed_newline.Ln.FWD.lower → ...es-save-AA.txt_fixed_newline.Ln.FWD.lower b/...es-save-AA.txt_fixed_newline.Ln.FWD.lower → ...es-save-AA.txt_fixed_newline.Ln.FWD.lower
diff --git a/...es-save-AA.txt_fixed_newline.Ln.FWD.upper → ...es-save-AA.txt_fixed_newline.Ln.FWD.upper b/...es-save-AA.txt_fixed_newline.Ln.FWD.upper → ...es-save-AA.txt_fixed_newline.Ln.FWD.upper
diff --git a/...tEval/pastebin.com_bbWXHaTn/iptables-save → ...tEval/pastebin.com_bbWXHaTn/iptables-save b/...tEval/pastebin.com_bbWXHaTn/iptables-save → ...tEval/pastebin.com_bbWXHaTn/iptables-save
diff --git a/...n.com_bbWXHaTn/iptables-save.Ln.FWD.lower → ...n.com_bbWXHaTn/iptables-save.Ln.FWD.lower b/...n.com_bbWXHaTn/iptables-save.Ln.FWD.lower → ...n.com_bbWXHaTn/iptables-save.Ln.FWD.lower
diff --git a/...n.com_bbWXHaTn/iptables-save.Ln.FWD.upper → ...n.com_bbWXHaTn/iptables-save.Ln.FWD.upper b/...n.com_bbWXHaTn/iptables-save.Ln.FWD.upper → ...n.com_bbWXHaTn/iptables-save.Ln.FWD.upper
diff --git a/...es/IPPartEval/rlworkman.net/iptables-save → ...es/IPPartEval/rlworkman.net/iptables-save b/...es/IPPartEval/rlworkman.net/iptables-save → ...es/IPPartEval/rlworkman.net/iptables-save
diff --git a/.../rlworkman.net/iptables-save.Ln.INP.lower → .../rlworkman.net/iptables-save.Ln.INP.lower b/.../rlworkman.net/iptables-save.Ln.INP.lower → .../rlworkman.net/iptables-save.Ln.INP.lower
diff --git a/.../rlworkman.net/iptables-save.Ln.INP.upper → .../rlworkman.net/iptables-save.Ln.INP.upper b/.../rlworkman.net/iptables-save.Ln.INP.upper → .../rlworkman.net/iptables-save.Ln.INP.upper
diff --git a/Examples/IPPartEval/sargon/iptables-save.txt → ...mples/IPPartEval/sargon/iptables-save.txt b/Examples/IPPartEval/sargon/iptables-save.txt → ...mples/IPPartEval/sargon/iptables-save.txt
diff --git a/...val/sargon/iptables-save.txt.Ln.INP.lower → ...val/sargon/iptables-save.txt.Ln.INP.lower b/...val/sargon/iptables-save.txt.Ln.INP.lower → ...val/sargon/iptables-save.txt.Ln.INP.lower
diff --git a/...val/sargon/iptables-save.txt.Ln.INP.upper → ...val/sargon/iptables-save.txt.Ln.INP.upper b/...val/sargon/iptables-save.txt.Ln.INP.upper → ...val/sargon/iptables-save.txt.Ln.INP.upper
diff --git a/Examples/IPPartEval/worst_case/iptables-save → ...mples/IPPartEval/worst_case/iptables-save b/Examples/IPPartEval/worst_case/iptables-save → ...mples/IPPartEval/worst_case/iptables-save
diff --git a/Examples/Parser_Test/Parser_Test.thy → thy/Examples/Parser_Test/Parser_Test.thy b/Examples/Parser_Test/Parser_Test.thy → thy/Examples/Parser_Test/Parser_Test.thy
diff --git a/Examples/Parser_Test/data/iptables-save → thy/Examples/Parser_Test/data/iptables-save b/Examples/Parser_Test/data/iptables-save → thy/Examples/Parser_Test/data/iptables-save
diff --git a/...ofsaturn_com/Analyze_Ringofsaturn_com.thy → ...ofsaturn_com/Analyze_Ringofsaturn_com.thy b/...ofsaturn_com/Analyze_Ringofsaturn_com.thy → ...ofsaturn_com/Analyze_Ringofsaturn_com.thy
diff --git a/Examples/Ringofsaturn_com/iptables-save → thy/Examples/Ringofsaturn_com/iptables-save b/Examples/Ringofsaturn_com/iptables-save → thy/Examples/Ringofsaturn_com/iptables-save
diff --git a/Examples/Ringofsaturn_com/iptables_Lnv → thy/Examples/Ringofsaturn_com/iptables_Lnv b/Examples/Ringofsaturn_com/iptables_Lnv → thy/Examples/Ringofsaturn_com/iptables_Lnv
diff --git a/Examples/Ringofsaturn_com/iptables_script.sh → ...mples/Ringofsaturn_com/iptables_script.sh b/Examples/Ringofsaturn_com/iptables_script.sh → ...mples/Ringofsaturn_com/iptables_script.sh
diff --git a/...015_aug_iptables-save-spoofing-protection → ...015_aug_iptables-save-spoofing-protection b/...015_aug_iptables-save-spoofing-protection → ...015_aug_iptables-save-spoofing-protection
diff --git a/...SQRL_Shorewall/Analyze_SQRL_Shorewall.thy → ...SQRL_Shorewall/Analyze_SQRL_Shorewall.thy b/...SQRL_Shorewall/Analyze_SQRL_Shorewall.thy → ...SQRL_Shorewall/Analyze_SQRL_Shorewall.thy
diff --git a/...ples/SQRL_Shorewall/SQRL_2015_nospoof.thy → ...ples/SQRL_Shorewall/SQRL_2015_nospoof.thy b/...ples/SQRL_Shorewall/SQRL_2015_nospoof.thy → ...ples/SQRL_Shorewall/SQRL_2015_nospoof.thy
diff --git a/Examples/SQRL_Shorewall/iptables-saveakachan → ...mples/SQRL_Shorewall/iptables-saveakachan b/Examples/SQRL_Shorewall/iptables-saveakachan → ...mples/SQRL_Shorewall/iptables-saveakachan
diff --git a/...on_DS414/Analyze_Synology_Diskstation.thy → ...on_DS414/Analyze_Synology_Diskstation.thy b/...on_DS414/Analyze_Synology_Diskstation.thy → ...on_DS414/Analyze_Synology_Diskstation.thy
diff --git a/.../Synology_Diskstation_DS414/iptables-save → .../Synology_Diskstation_DS414/iptables-save b/.../Synology_Diskstation_DS414/iptables-save → .../Synology_Diskstation_DS414/iptables-save
diff --git a/...ology_Diskstation_DS414/iptables_Ln_tuned → ...ology_Diskstation_DS414/iptables_Ln_tuned b/...ology_Diskstation_DS414/iptables_Ln_tuned → ...ology_Diskstation_DS414/iptables_Ln_tuned
diff --git a/...tation_DS414/iptables_Ln_tuned_parsed.thy → ...tation_DS414/iptables_Ln_tuned_parsed.thy b/...tation_DS414/iptables_Ln_tuned_parsed.thy → ...tation_DS414/iptables_Ln_tuned_parsed.thy
diff --git a/Examples/Synology_Diskstation_DS414/uname_a → ...amples/Synology_Diskstation_DS414/uname_a b/Examples/Synology_Diskstation_DS414/uname_a → ...amples/Synology_Diskstation_DS414/uname_a
diff --git a/...Net_Firewall/Analyze_TUM_Net_Firewall.thy → ...Net_Firewall/Analyze_TUM_Net_Firewall.thy b/...Net_Firewall/Analyze_TUM_Net_Firewall.thy → ...Net_Firewall/Analyze_TUM_Net_Firewall.thy
diff --git a/Examples/TUM_Net_Firewall/README_cheating → ...Examples/TUM_Net_Firewall/README_cheating b/Examples/TUM_Net_Firewall/README_cheating → ...Examples/TUM_Net_Firewall/README_cheating
diff --git a/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy → ...amples/TUM_Net_Firewall/TUM_Simple_FW.thy b/Examples/TUM_Net_Firewall/TUM_Simple_FW.thy → ...amples/TUM_Net_Firewall/TUM_Simple_FW.thy
diff --git a/...es/TUM_Net_Firewall/TUM_Spoofing_new3.thy → ...es/TUM_Net_Firewall/TUM_Spoofing_new3.thy b/...es/TUM_Net_Firewall/TUM_Spoofing_new3.thy → ...es/TUM_Net_Firewall/TUM_Spoofing_new3.thy
diff --git a/...ptables-save-2015-05-13_10-53-20_cheating → ...ptables-save-2015-05-13_10-53-20_cheating b/...ptables-save-2015-05-13_10-53-20_cheating → ...ptables-save-2015-05-13_10-53-20_cheating
diff --git a/...ptables-save-2015-05-15_14-14-46_cheating → ...ptables-save-2015-05-15_14-14-46_cheating b/...ptables-save-2015-05-15_14-14-46_cheating → ...ptables-save-2015-05-15_14-14-46_cheating
diff --git a/...ptables-save-2015-05-15_15-23-41_cheating → ...ptables-save-2015-05-15_15-23-41_cheating b/...ptables-save-2015-05-15_15-23-41_cheating → ...ptables-save-2015-05-15_15-23-41_cheating
diff --git a/..._Firewall/iptables_Ln_29.11.2013_cheating → ..._Firewall/iptables_Ln_29.11.2013_cheating b/..._Firewall/iptables_Ln_29.11.2013_cheating → ..._Firewall/iptables_Ln_29.11.2013_cheating
diff --git a/...rewall/iptables_Ln_29.11.2013_cheating.ML → ...rewall/iptables_Ln_29.11.2013_cheating.ML b/...rewall/iptables_Ln_29.11.2013_cheating.ML → ...rewall/iptables_Ln_29.11.2013_cheating.ML
diff --git a/Examples/TUM_Net_Firewall/unfold_code.ML → thy/Examples/TUM_Net_Firewall/unfold_code.ML b/Examples/TUM_Net_Firewall/unfold_code.ML → thy/Examples/TUM_Net_Firewall/unfold_code.ML
diff --git a/Examples/generated_code/.empty_dir → thy/Examples/generated_code/.empty_dir b/Examples/generated_code/.empty_dir → thy/Examples/generated_code/.empty_dir
diff --git a/.../sns.ias.edu/SNS_IAS_Eduroam_Spoofing.thy → .../sns.ias.edu/SNS_IAS_Eduroam_Spoofing.thy b/.../sns.ias.edu/SNS_IAS_Eduroam_Spoofing.thy → .../sns.ias.edu/SNS_IAS_Eduroam_Spoofing.thy
diff --git a/Examples/sns.ias.edu/eduroam_iptables-save → ...xamples/sns.ias.edu/eduroam_iptables-save b/Examples/sns.ias.edu/eduroam_iptables-save → ...xamples/sns.ias.edu/eduroam_iptables-save
diff --git a/Examples/sns.ias.edu/iptables_Lnv → thy/Examples/sns.ias.edu/iptables_Lnv b/Examples/sns.ias.edu/iptables_Lnv → thy/Examples/sns.ias.edu/iptables_Lnv
diff --git a/Examples/sns.ias.edu/test.sh → thy/Examples/sns.ias.edu/test.sh b/Examples/sns.ias.edu/test.sh → thy/Examples/sns.ias.edu/test.sh
diff --git a/Firewall_Common.thy → thy/Firewall_Common.thy b/Firewall_Common.thy → thy/Firewall_Common.thy
diff --git a/Firewall_Common_Decision_State.thy → thy/Firewall_Common_Decision_State.thy b/Firewall_Common_Decision_State.thy → thy/Firewall_Common_Decision_State.thy
diff --git a/Iptables_Semantics.thy → thy/Iptables_Semantics.thy b/Iptables_Semantics.thy → thy/Iptables_Semantics.thy
diff --git a/Matching.thy → thy/Matching.thy b/Matching.thy → thy/Matching.thy
diff --git a/Matching_Embeddings.thy → thy/Matching_Embeddings.thy b/Matching_Embeddings.thy → thy/Matching_Embeddings.thy
diff --git a/Misc.thy → thy/Misc.thy b/Misc.thy → thy/Misc.thy
diff --git a/No_Spoof_Embeddings.thy → thy/No_Spoof_Embeddings.thy b/No_Spoof_Embeddings.thy → thy/No_Spoof_Embeddings.thy
diff --git a/Primitive_Matchers/Code_Interface.thy → thy/Primitive_Matchers/Code_Interface.thy b/Primitive_Matchers/Code_Interface.thy → thy/Primitive_Matchers/Code_Interface.thy
diff --git a/...tive_Matchers/Common_Primitive_Lemmas.thy → ...tive_Matchers/Common_Primitive_Lemmas.thy b/...tive_Matchers/Common_Primitive_Lemmas.thy → ...tive_Matchers/Common_Primitive_Lemmas.thy
diff --git a/...ive_Matchers/Common_Primitive_Matcher.thy → ...ive_Matchers/Common_Primitive_Matcher.thy b/...ive_Matchers/Common_Primitive_Matcher.thy → ...ive_Matchers/Common_Primitive_Matcher.thy
diff --git a/...tive_Matchers/Common_Primitive_Syntax.thy → ...tive_Matchers/Common_Primitive_Syntax.thy b/...tive_Matchers/Common_Primitive_Syntax.thy → ...tive_Matchers/Common_Primitive_Syntax.thy
diff --git a/...ve_Matchers/Common_Primitive_toString.thy → ...ve_Matchers/Common_Primitive_toString.thy b/...ve_Matchers/Common_Primitive_toString.thy → ...ve_Matchers/Common_Primitive_toString.thy
diff --git a/Primitive_Matchers/Conntrack_State.thy → thy/Primitive_Matchers/Conntrack_State.thy b/Primitive_Matchers/Conntrack_State.thy → thy/Primitive_Matchers/Conntrack_State.thy
diff --git a/...ve_Matchers/Conntrack_State_Transform.thy → ...ve_Matchers/Conntrack_State_Transform.thy b/...ve_Matchers/Conntrack_State_Transform.thy → ...ve_Matchers/Conntrack_State_Transform.thy
diff --git a/Primitive_Matchers/Iface.thy → thy/Primitive_Matchers/Iface.thy b/Primitive_Matchers/Iface.thy → thy/Primitive_Matchers/Iface.thy
diff --git a/Primitive_Matchers/Iface_Attic.thy → thy/Primitive_Matchers/Iface_Attic.thy b/Primitive_Matchers/Iface_Attic.thy → thy/Primitive_Matchers/Iface_Attic.thy
diff --git a/Primitive_Matchers/Interface_Replace.thy → thy/Primitive_Matchers/Interface_Replace.thy b/Primitive_Matchers/Interface_Replace.thy → thy/Primitive_Matchers/Interface_Replace.thy
diff --git a/Primitive_Matchers/IpAddresses.thy → thy/Primitive_Matchers/IpAddresses.thy b/Primitive_Matchers/IpAddresses.thy → thy/Primitive_Matchers/IpAddresses.thy
diff --git a/Primitive_Matchers/IpAddresses_Normalize.thy → ...mitive_Matchers/IpAddresses_Normalize.thy b/Primitive_Matchers/IpAddresses_Normalize.thy → ...mitive_Matchers/IpAddresses_Normalize.thy
diff --git a/Primitive_Matchers/Ipassmt.thy → thy/Primitive_Matchers/Ipassmt.thy b/Primitive_Matchers/Ipassmt.thy → thy/Primitive_Matchers/Ipassmt.thy
diff --git a/Primitive_Matchers/No_Spoof.thy → thy/Primitive_Matchers/No_Spoof.thy b/Primitive_Matchers/No_Spoof.thy → thy/Primitive_Matchers/No_Spoof.thy
diff --git a/Primitive_Matchers/Parser.thy → thy/Primitive_Matchers/Parser.thy b/Primitive_Matchers/Parser.thy → thy/Primitive_Matchers/Parser.thy
diff --git a/Primitive_Matchers/Ports.thy → thy/Primitive_Matchers/Ports.thy b/Primitive_Matchers/Ports.thy → thy/Primitive_Matchers/Ports.thy
diff --git a/Primitive_Matchers/Ports_Normalize.thy → thy/Primitive_Matchers/Ports_Normalize.thy b/Primitive_Matchers/Ports_Normalize.thy → thy/Primitive_Matchers/Ports_Normalize.thy
diff --git a/Primitive_Matchers/Primitive_Abstract.thy → ...Primitive_Matchers/Primitive_Abstract.thy b/Primitive_Matchers/Primitive_Abstract.thy → ...Primitive_Matchers/Primitive_Abstract.thy
diff --git a/Primitive_Matchers/Protocol.thy → thy/Primitive_Matchers/Protocol.thy b/Primitive_Matchers/Protocol.thy → thy/Primitive_Matchers/Protocol.thy
diff --git a/Primitive_Matchers/README → thy/Primitive_Matchers/README b/Primitive_Matchers/README → thy/Primitive_Matchers/README
diff --git a/Primitive_Matchers/Simple_Packet.thy → thy/Primitive_Matchers/Simple_Packet.thy b/Primitive_Matchers/Simple_Packet.thy → thy/Primitive_Matchers/Simple_Packet.thy
diff --git a/Primitive_Matchers/Transform.thy → thy/Primitive_Matchers/Transform.thy b/Primitive_Matchers/Transform.thy → thy/Primitive_Matchers/Transform.thy
diff --git a/ROOT → thy/ROOT b/ROOT → thy/ROOT
diff --git a/thy/ROOTS b/thy/ROOTS
@@ -0,0 +1 @@
+Bitmagic
diff --git a/Ruleset_Update.thy → thy/Ruleset_Update.thy b/Ruleset_Update.thy → thy/Ruleset_Update.thy
diff --git a/Semantics.thy → thy/Semantics.thy b/Semantics.thy → thy/Semantics.thy
diff --git a/Semantics_Embeddings.thy → thy/Semantics_Embeddings.thy b/Semantics_Embeddings.thy → thy/Semantics_Embeddings.thy
diff --git a/Semantics_Goto.thy → thy/Semantics_Goto.thy b/Semantics_Goto.thy → thy/Semantics_Goto.thy
diff --git a/Semantics_Stateful.thy → thy/Semantics_Stateful.thy b/Semantics_Stateful.thy → thy/Semantics_Stateful.thy
diff --git a/Semantics_Ternary/Fixed_Action.thy → thy/Semantics_Ternary/Fixed_Action.thy b/Semantics_Ternary/Fixed_Action.thy → thy/Semantics_Ternary/Fixed_Action.thy
diff --git a/Semantics_Ternary/Matching_Ternary.thy → thy/Semantics_Ternary/Matching_Ternary.thy b/Semantics_Ternary/Matching_Ternary.thy → thy/Semantics_Ternary/Matching_Ternary.thy
diff --git a/Semantics_Ternary/Negation_Type_Matching.thy → ...antics_Ternary/Negation_Type_Matching.thy b/Semantics_Ternary/Negation_Type_Matching.thy → ...antics_Ternary/Negation_Type_Matching.thy
diff --git a/Semantics_Ternary/Normalized_Matches.thy → thy/Semantics_Ternary/Normalized_Matches.thy b/Semantics_Ternary/Normalized_Matches.thy → thy/Semantics_Ternary/Normalized_Matches.thy
diff --git a/Semantics_Ternary/Optimizing.thy → thy/Semantics_Ternary/Optimizing.thy b/Semantics_Ternary/Optimizing.thy → thy/Semantics_Ternary/Optimizing.thy
diff --git a/Semantics_Ternary/Packet_Set.thy → thy/Semantics_Ternary/Packet_Set.thy b/Semantics_Ternary/Packet_Set.thy → thy/Semantics_Ternary/Packet_Set.thy
diff --git a/Semantics_Ternary/Packet_Set_Impl.thy → thy/Semantics_Ternary/Packet_Set_Impl.thy b/Semantics_Ternary/Packet_Set_Impl.thy → thy/Semantics_Ternary/Packet_Set_Impl.thy
diff --git a/...ntics_Ternary/Primitive_Normalization.thy → ...ntics_Ternary/Primitive_Normalization.thy b/...ntics_Ternary/Primitive_Normalization.thy → ...ntics_Ternary/Primitive_Normalization.thy
diff --git a/Semantics_Ternary/Semantics_Ternary.thy → thy/Semantics_Ternary/Semantics_Ternary.thy b/Semantics_Ternary/Semantics_Ternary.thy → thy/Semantics_Ternary/Semantics_Ternary.thy
diff --git a/Semantics_Ternary/Unknown_Match_Tacs.thy → thy/Semantics_Ternary/Unknown_Match_Tacs.thy b/Semantics_Ternary/Unknown_Match_Tacs.thy → thy/Semantics_Ternary/Unknown_Match_Tacs.thy
diff --git a/Simple_Firewall/IPPartitioning.thy → thy/Simple_Firewall/IPPartitioning.thy b/Simple_Firewall/IPPartitioning.thy → thy/Simple_Firewall/IPPartitioning.thy
diff --git a/Simple_Firewall/Shadowed.thy → thy/Simple_Firewall/Shadowed.thy b/Simple_Firewall/Shadowed.thy → thy/Simple_Firewall/Shadowed.thy
diff --git a/Simple_Firewall/SimpleFw_Compliance.thy → thy/Simple_Firewall/SimpleFw_Compliance.thy b/Simple_Firewall/SimpleFw_Compliance.thy → thy/Simple_Firewall/SimpleFw_Compliance.thy
diff --git a/Simple_Firewall/SimpleFw_Semantics.thy → thy/Simple_Firewall/SimpleFw_Semantics.thy b/Simple_Firewall/SimpleFw_Semantics.thy → thy/Simple_Firewall/SimpleFw_Semantics.thy
diff --git a/Simple_Firewall/SimpleFw_toString.thy → thy/Simple_Firewall/SimpleFw_toString.thy b/Simple_Firewall/SimpleFw_toString.thy → thy/Simple_Firewall/SimpleFw_toString.thy
diff --git a/afp/Mergesort.thy → thy/afp/Mergesort.thy b/afp/Mergesort.thy → thy/afp/Mergesort.thy
diff --git a/document/mathpartir.sty → thy/document/mathpartir.sty b/document/mathpartir.sty → thy/document/mathpartir.sty
diff --git a/document/root.tex → thy/document/root.tex b/document/root.tex → thy/document/root.tex