diff --git a/thys/Public_Announcement_Logic/PAL.thy b/thys/Public_Announcement_Logic/PAL.thy
new file mode 100644
--- /dev/null
+++ b/thys/Public_Announcement_Logic/PAL.thy
@@ -0,0 +1,465 @@
+(*
+  File:      PAL.thy
+  Author:    Asta Halkjær From
+
+  This work is a formalization of public announcement logic with countably many agents.
+  It includes proofs of soundness and completeness for a variant of the axiom system
+    PA + DIST! + NEC!.
+  The completeness proof builds on the Epistemic Logic theory.
+*)
+
+theory PAL imports "Epistemic_Logic.Epistemic_Logic" begin
+
+section \<open>Syntax\<close>
+
+datatype 'i pfm
+  = FF ("\<^bold>\<bottom>\<^sub>!")
+  | Pro' id ("Pro\<^sub>!")
+  | Dis \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr "\<^bold>\<or>\<^sub>!" 30)
+  | Con \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr "\<^bold>\<and>\<^sub>!" 35)
+  | Imp \<open>'i pfm\<close> \<open>'i pfm\<close> (infixr "\<^bold>\<longrightarrow>\<^sub>!" 25)
+  | K' 'i \<open>'i pfm\<close> ("K\<^sub>!")
+  | Ann \<open>'i pfm\<close> \<open>'i pfm\<close> ("[_]\<^sub>! _" [50, 50] 50)
+
+abbreviation PIff :: \<open>'i pfm \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> (infixr "\<^bold>\<longleftrightarrow>\<^sub>!" 25) where
+  \<open>p \<^bold>\<longleftrightarrow>\<^sub>! q \<equiv> (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<and>\<^sub>! (q \<^bold>\<longrightarrow>\<^sub>! p)\<close>
+
+section \<open>Semantics\<close>
+
+fun
+  psemantics :: \<open>('i, 'w) kripke \<Rightarrow> 'w \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> ("_, _ \<Turnstile>\<^sub>! _" [50, 50] 50) and
+  restrict :: \<open>('i, 'w) kripke \<Rightarrow> 'i pfm \<Rightarrow> ('i, 'w) kripke\<close> where
+  \<open>(M, w \<Turnstile>\<^sub>! \<^bold>\<bottom>\<^sub>!) = False\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! Pro\<^sub>! x) = \<pi> M w x\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<or>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<or> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<and> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)) = ((M, w \<Turnstile>\<^sub>! p) \<longrightarrow> (M, w \<Turnstile>\<^sub>! q))\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! K\<^sub>! i p) = (\<forall>v \<in> \<K> M i w. M, v \<Turnstile>\<^sub>! p)\<close>
+| \<open>(M, w \<Turnstile>\<^sub>! [r]\<^sub>! p) = ((M, w \<Turnstile>\<^sub>! r) \<longrightarrow> (restrict M r, w \<Turnstile>\<^sub>! p))\<close>
+| \<open>restrict M p = Kripke (\<pi> M) (\<lambda>i w. {v. v \<in> \<K> M i w \<and> (M, v \<Turnstile>\<^sub>! p)})\<close>
+
+primrec static :: \<open>'i pfm \<Rightarrow> bool\<close> where
+  \<open>static \<^bold>\<bottom>\<^sub>! = True\<close>
+| \<open>static (Pro\<^sub>! _) = True\<close>
+| \<open>static (p \<^bold>\<or>\<^sub>! q) = (static p \<and> static q)\<close>
+| \<open>static (p \<^bold>\<and>\<^sub>! q) = (static p \<and> static q)\<close>
+| \<open>static (p \<^bold>\<longrightarrow>\<^sub>! q) = (static p \<and> static q)\<close>
+| \<open>static (K\<^sub>! i p) = static p\<close>
+| \<open>static ([r]\<^sub>! p) = False\<close>
+
+primrec lower :: \<open>'i pfm \<Rightarrow> 'i fm\<close> where
+  \<open>lower \<^bold>\<bottom>\<^sub>! = \<^bold>\<bottom>\<close>
+| \<open>lower (Pro\<^sub>! x) = Pro x\<close>
+| \<open>lower (p \<^bold>\<or>\<^sub>! q) = (lower p \<^bold>\<or> lower q)\<close>
+| \<open>lower (p \<^bold>\<and>\<^sub>! q) = (lower p \<^bold>\<and> lower q)\<close>
+| \<open>lower (p \<^bold>\<longrightarrow>\<^sub>! q) = (lower p \<^bold>\<longrightarrow> lower q)\<close>
+| \<open>lower (K\<^sub>! i p) = K i (lower p)\<close>
+| \<open>lower ([r]\<^sub>! p) = undefined\<close>
+
+primrec lift :: \<open>'i fm \<Rightarrow> 'i pfm\<close> where
+  \<open>lift \<^bold>\<bottom> = \<^bold>\<bottom>\<^sub>!\<close>
+| \<open>lift (Pro x) = Pro\<^sub>! x\<close>
+| \<open>lift (p \<^bold>\<or> q) = (lift p \<^bold>\<or>\<^sub>! lift q)\<close>
+| \<open>lift (p \<^bold>\<and> q) = (lift p \<^bold>\<and>\<^sub>! lift q)\<close>
+| \<open>lift (p \<^bold>\<longrightarrow> q) = (lift p \<^bold>\<longrightarrow>\<^sub>! lift q)\<close>
+| \<open>lift (K i p) = K\<^sub>! i (lift p)\<close>
+
+lemma lower_semantics:
+  assumes \<open>static p\<close>
+  shows \<open>(M, w \<Turnstile> lower p) \<longleftrightarrow> (M, w \<Turnstile>\<^sub>! p)\<close>
+  using assms by (induct p arbitrary: w) simp_all
+
+lemma lift_semantics: \<open>(M, w \<Turnstile> p) \<longleftrightarrow> (M, w \<Turnstile>\<^sub>! lift p)\<close>
+  by (induct p arbitrary: w) simp_all
+
+lemma lower_lift: \<open>lower (lift p) = p\<close>
+  by (induct p) simp_all
+
+lemma lift_lower: \<open>static p \<Longrightarrow> lift (lower p) = p\<close>
+  by (induct p) simp_all
+
+section \<open>Soundness of Reduction\<close>
+
+primrec reduce' :: \<open>'i pfm \<Rightarrow> 'i pfm \<Rightarrow> 'i pfm\<close> where
+  \<open>reduce' r \<^bold>\<bottom>\<^sub>! = (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)\<close>
+| \<open>reduce' r (Pro\<^sub>! x) = (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)\<close>
+| \<open>reduce' r (p \<^bold>\<or>\<^sub>! q) = (reduce' r p \<^bold>\<or>\<^sub>! reduce' r q)\<close>
+| \<open>reduce' r (p \<^bold>\<and>\<^sub>! q) = (reduce' r p \<^bold>\<and>\<^sub>! reduce' r q)\<close>
+| \<open>reduce' r (p \<^bold>\<longrightarrow>\<^sub>! q) = (reduce' r p \<^bold>\<longrightarrow>\<^sub>! reduce' r q)\<close>
+| \<open>reduce' r (K\<^sub>! i p) = (r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce' r p))\<close>
+| \<open>reduce' r ([p]\<^sub>! q) = undefined\<close>
+
+primrec reduce :: \<open>'i pfm \<Rightarrow> 'i pfm\<close> where
+  \<open>reduce \<^bold>\<bottom>\<^sub>! = \<^bold>\<bottom>\<^sub>!\<close>
+| \<open>reduce (Pro\<^sub>! x) = Pro\<^sub>! x\<close>
+| \<open>reduce (p \<^bold>\<or>\<^sub>! q) = (reduce p \<^bold>\<or>\<^sub>! reduce q)\<close>
+| \<open>reduce (p \<^bold>\<and>\<^sub>! q) = (reduce p \<^bold>\<and>\<^sub>! reduce q)\<close>
+| \<open>reduce (p \<^bold>\<longrightarrow>\<^sub>! q) = (reduce p \<^bold>\<longrightarrow>\<^sub>! reduce q)\<close>
+| \<open>reduce (K\<^sub>! i p) = K\<^sub>! i (reduce p)\<close>
+| \<open>reduce ([r]\<^sub>! p) = reduce' (reduce r) (reduce p)\<close>
+
+lemma static_reduce': \<open>static p \<Longrightarrow> static r \<Longrightarrow> static (reduce' r p)\<close>
+  by (induct p) simp_all
+
+lemma static_reduce: \<open>static (reduce p)\<close>
+  by (induct p) (simp_all add: static_reduce')
+
+lemma reduce'_semantics:
+  assumes \<open>static q\<close>
+  shows \<open>((M, w \<Turnstile>\<^sub>! [p]\<^sub>! (q))) = (M, w \<Turnstile>\<^sub>! reduce' p q)\<close>
+  using assms by (induct q arbitrary: w) auto
+
+lemma reduce_semantics: \<open>(M, w \<Turnstile>\<^sub>! p) = (M, w \<Turnstile>\<^sub>! reduce p)\<close>
+proof (induct p arbitrary: M w)
+  case (Ann p q)
+  then show ?case
+    using reduce'_semantics static_reduce by fastforce
+qed auto
+
+section \<open>Proof System\<close>
+
+primrec peval :: \<open>(id \<Rightarrow> bool) \<Rightarrow> ('i pfm \<Rightarrow> bool) \<Rightarrow> 'i pfm \<Rightarrow> bool\<close> where
+  \<open>peval _ _ \<^bold>\<bottom>\<^sub>! = False\<close>
+| \<open>peval g _ (Pro\<^sub>! x) = g x\<close>
+| \<open>peval g h (p \<^bold>\<or>\<^sub>! q) = (peval g h p \<or> peval g h q)\<close>
+| \<open>peval g h (p \<^bold>\<and>\<^sub>! q) = (peval g h p \<and> peval g h q)\<close>
+| \<open>peval g h (p \<^bold>\<longrightarrow>\<^sub>! q) = (peval g h p \<longrightarrow> peval g h q)\<close>
+| \<open>peval _ h (K\<^sub>! i p) = h (K\<^sub>! i p)\<close>
+| \<open>peval _ h ([r]\<^sub>! p) = h ([r]\<^sub>! p)\<close>
+
+abbreviation \<open>ptautology p \<equiv> \<forall>g h. peval g h p\<close>
+
+inductive PA :: \<open>'i pfm \<Rightarrow> bool\<close> ("\<turnstile>\<^sub>! _" [50] 50) where
+  PA1: \<open>ptautology p \<Longrightarrow> \<turnstile>\<^sub>! p\<close>
+| PA2: \<open>\<turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q)\<close>
+| PR1: \<open>\<turnstile>\<^sub>! p \<Longrightarrow> \<turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q) \<Longrightarrow> \<turnstile>\<^sub>! q\<close>
+| PR2: \<open>\<turnstile>\<^sub>! p \<Longrightarrow> \<turnstile>\<^sub>! K\<^sub>! i p\<close>
+| PR3: \<open>\<turnstile>\<^sub>! p \<Longrightarrow> \<turnstile>\<^sub>! [r]\<^sub>! p\<close>
+| PFF: \<open>\<turnstile>\<^sub>! ([r]\<^sub>! \<^bold>\<bottom>\<^sub>! \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!))\<close>
+| PPro: \<open>\<turnstile>\<^sub>! ([r]\<^sub>! Pro\<^sub>! x \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x))\<close>
+| PDis: \<open>\<turnstile>\<^sub>! ([r]\<^sub>! (p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q)\<close>
+| PCon: \<open>\<turnstile>\<^sub>! ([r]\<^sub>! (p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q)\<close>
+| PImp: \<open>\<turnstile>\<^sub>! (([r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q))\<close>
+| PK: \<open>\<turnstile>\<^sub>! (([r]\<^sub>! K\<^sub>! i p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p)))\<close>
+
+lemma eval_peval: \<open>eval h (g o lift) p = peval h g (lift p)\<close>
+  by (induct p) simp_all
+
+lemma tautology_ptautology: \<open>tautology p \<Longrightarrow> ptautology (lift p)\<close>
+  using eval_peval by blast
+
+lemma peval_eval:
+  assumes \<open>static p\<close>
+  shows \<open>eval h g (lower p) = peval h (g o lower) p\<close>
+  using assms by (induct p) simp_all
+
+lemma ptautology_tautology:
+  assumes \<open>static p\<close>
+  shows \<open>ptautology p \<Longrightarrow> tautology (lower p)\<close>
+  using assms peval_eval by blast
+
+theorem SystemK_PAK: \<open>\<turnstile> p \<Longrightarrow> \<turnstile>\<^sub>! lift p\<close>
+  by (induct p rule: SystemK.induct) (auto intro: PA.intros(1-5) simp: tautology_ptautology)
+
+theorem static_completeness:
+  assumes \<open>static p\<close> \<open>\<forall>(M :: ('i :: countable, 'i fm set) kripke) w. M, w \<Turnstile>\<^sub>! p\<close>
+  shows \<open>\<turnstile>\<^sub>! p\<close>
+proof -
+  have \<open>\<forall>(M :: ('i :: countable, 'i fm set) kripke) w. M, w \<Turnstile> lower p\<close>
+    using assms by (simp add: lower_semantics)
+  then have \<open>\<turnstile> lower p\<close>
+    by (simp add: completeness)
+  then have \<open>\<turnstile>\<^sub>! lift (lower p)\<close>
+    using SystemK_PAK by fast
+  then show ?thesis
+    using assms(1) lift_lower by metis
+qed
+
+section \<open>Soundness\<close>
+
+lemma peval_semantics: \<open>peval (val w) (\<lambda>q. Kripke val r, w \<Turnstile>\<^sub>! q) p = (Kripke val r, w \<Turnstile>\<^sub>! p)\<close>
+  by (induct p) simp_all
+
+lemma ptautology:
+  assumes \<open>ptautology p\<close>
+  shows \<open>M, w \<Turnstile>\<^sub>! p\<close>
+proof -
+  from assms have \<open>peval (g w) (\<lambda>q. Kripke g r, w \<Turnstile>\<^sub>! q) p\<close> for g r
+    by simp
+  then have \<open>Kripke g r, w \<Turnstile>\<^sub>! p\<close> for g r
+    using peval_semantics by fast
+  then show \<open>M, w \<Turnstile>\<^sub>! p\<close>
+    by (metis kripke.collapse)
+qed
+
+theorem soundness:
+  assumes \<open>\<turnstile>\<^sub>! p\<close>
+  shows \<open>M, w \<Turnstile>\<^sub>! p\<close>
+  using assms by (induct p arbitrary: M w rule: PA.induct) (simp_all add: ptautology)
+
+section \<open>Completeness\<close>
+
+lemma ConE:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q)\<close>
+  shows \<open>\<turnstile>\<^sub>! p\<close> \<open>\<turnstile>\<^sub>! q\<close>
+  using assms by (metis PA1 PR1 peval.simps(4-5))+
+
+lemma Iff_Dis:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p')\<close> \<open>\<turnstile>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q')\<close>
+  shows \<open>\<turnstile>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q'))\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<or>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<or>\<^sub>! q')))\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma Iff_Con:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p')\<close> \<open>\<turnstile>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q')\<close>
+  shows \<open>\<turnstile>\<^sub>! ((p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q'))\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<and>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<and>\<^sub>! q')))\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma Iff_Imp:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p')\<close> \<open>\<turnstile>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q')\<close>
+  shows \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q'))\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! q') \<^bold>\<longrightarrow>\<^sub>! ((p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (p' \<^bold>\<longrightarrow>\<^sub>! q')))\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma Iff_sym: \<open>(\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q)) = (\<turnstile>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! p))\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! (q \<^bold>\<longleftrightarrow>\<^sub>! p))\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using PR1 ConE by blast
+qed
+
+lemma Iff_Iff:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p')\<close> \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q)\<close>
+  shows \<open>\<turnstile>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q)\<close>
+proof -
+  have \<open>ptautology ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q))\<close>
+    by (metis peval.simps(4-5))
+  with PA1 have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! p') \<^bold>\<longrightarrow>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! (p' \<^bold>\<longleftrightarrow>\<^sub>! q))\<close> .
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma K'_A2': \<open>\<turnstile>\<^sub>! (K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q)\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<and>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q)\<close>
+    using PA2 by fast
+  moreover have \<open>\<turnstile>\<^sub>! ((P \<^bold>\<and>\<^sub>! Q \<^bold>\<longrightarrow>\<^sub>! R) \<^bold>\<longrightarrow>\<^sub>! (Q \<^bold>\<longrightarrow>\<^sub>! P \<^bold>\<longrightarrow>\<^sub>! R))\<close> for P Q R :: \<open>'i pfm\<close>
+    by (simp add: PA1)
+  ultimately show ?thesis
+    using PR1 by fast
+qed
+
+lemma K'_map:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  shows \<open>\<turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q)\<close>
+proof -
+  note \<open>\<turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+  then have \<open>\<turnstile>\<^sub>! K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q)\<close>
+    using PR2 by fast
+  moreover have \<open>\<turnstile>\<^sub>! (K\<^sub>! i (p \<^bold>\<longrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i q)\<close>
+    using K'_A2' by fast
+  ultimately show ?thesis
+    using PR1 by fast
+qed
+
+lemma ConI:
+  assumes \<open>\<turnstile>\<^sub>! p\<close> \<open>\<turnstile>\<^sub>! q\<close>
+  shows \<open>\<turnstile>\<^sub>! (p \<^bold>\<and>\<^sub>! q)\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q \<^bold>\<longrightarrow>\<^sub>! p \<^bold>\<and>\<^sub>! q)\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma Iff_wk:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! q)\<close>
+  shows \<open>\<turnstile>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q))\<close>
+proof -
+  have \<open>\<turnstile>\<^sub>! ((p \<^bold>\<longleftrightarrow>\<^sub>! q) \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! (r \<^bold>\<longrightarrow>\<^sub>! q)))\<close>
+    by (simp add: PA1)
+  then show ?thesis
+    using assms PR1 by blast
+qed
+
+lemma Iff_reduce':
+  assumes \<open>static p\<close>
+  shows \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p)\<close>
+  using assms
+proof (induct p rule: pfm.induct)
+  case FF
+  then show ?case
+    by (simp add: PFF)
+next
+  case (Pro' x)
+  then show ?case
+    by (simp add: PPro)
+next
+  case (Dis p q)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<or>\<^sub>! q))\<close>
+    using Iff_Dis by force
+  moreover have \<open>\<turnstile>\<^sub>! (([r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<or>\<^sub>! q)))\<close>
+    using PDis Iff_sym by fastforce
+  ultimately show ?case
+    using PA1 PR1 Iff_Iff by blast
+next
+  case (Con p q)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<and>\<^sub>! q))\<close>
+    using Iff_Con by force
+  moreover have \<open>\<turnstile>\<^sub>! (([r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<and>\<^sub>! q)))\<close>
+    using PCon Iff_sym by fastforce
+  ultimately show ?case
+    using PA1 PR1 Iff_Iff by blast
+next
+  case (Imp p q)
+  then have \<open>\<turnstile>\<^sub>! (([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! reduce' r (p \<^bold>\<longrightarrow>\<^sub>! q))\<close>
+    using Iff_Imp by force
+  moreover have \<open>\<turnstile>\<^sub>! (([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r]\<^sub>! (p \<^bold>\<longrightarrow>\<^sub>! q)))\<close>
+    using PImp Iff_sym by fastforce
+  ultimately show ?case
+    using PA1 PR1 Iff_Iff by blast
+next
+  case (K' i p)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' r p)\<close>
+    by simp
+  then have \<open>\<turnstile>\<^sub>! (K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce' r p))\<close>
+    using K'_map ConE ConI by metis
+  moreover have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i ([r]\<^sub>! p))\<close>
+    using PK .
+  ultimately have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! r \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce' r p))\<close>
+    by (meson Iff_Iff Iff_sym Iff_wk)
+  then show ?case
+    by simp
+next
+  case (Ann r p)
+  then show ?case
+    by simp
+qed
+
+lemma Iff_Ann1:
+  assumes r: \<open>\<turnstile>\<^sub>! (r \<^bold>\<longleftrightarrow>\<^sub>! r')\<close> and \<open>static p\<close>
+  shows \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p)\<close>
+  using assms(2-)
+proof (induct p)
+  case FF
+  have \<open>\<turnstile>\<^sub>! ((r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!)))\<close>
+    by (auto intro: PA1)
+  then have \<open>\<turnstile>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! \<^bold>\<bottom>\<^sub>!))\<close>
+    using r PR1 by blast
+  then show ?case
+    by (meson PFF Iff_Iff Iff_sym)
+next
+  case (Pro' x)
+  have \<open>\<turnstile>\<^sub>! ((r \<^bold>\<longleftrightarrow>\<^sub>! r') \<^bold>\<longrightarrow>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x)))\<close>
+    by (auto intro: PA1)
+  then have \<open>\<turnstile>\<^sub>! ((r \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x) \<^bold>\<longleftrightarrow>\<^sub>! (r' \<^bold>\<longrightarrow>\<^sub>! Pro\<^sub>! x))\<close>
+    using r PR1 by blast
+  then show ?case
+    by (meson PPro Iff_Iff Iff_sym)
+next
+  case (Dis p q)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<or>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<or>\<^sub>! [r']\<^sub>! q)\<close>
+    by (simp add: Iff_Dis)
+  then show ?case
+    by (meson PDis Iff_Iff Iff_sym)
+next
+  case (Con p q)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<and>\<^sub>! [r]\<^sub>! q \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p \<^bold>\<and>\<^sub>! [r']\<^sub>! q)\<close>
+    by (simp add: Iff_Con)
+  then show ?case
+    by (meson PCon Iff_Iff Iff_sym)
+next
+  case (Imp p q)
+  then have \<open>\<turnstile>\<^sub>! (([r]\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r]\<^sub>! q) \<^bold>\<longleftrightarrow>\<^sub>! ([r']\<^sub>! p \<^bold>\<longrightarrow>\<^sub>! [r']\<^sub>! q))\<close>
+    by (simp add: Iff_Imp)
+  then show ?case
+    by (meson PImp Iff_Iff Iff_sym)
+next
+  case (K' i p)
+  then have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r']\<^sub>! p)\<close>
+    by simp
+  then have \<open>\<turnstile>\<^sub>! (K\<^sub>! i ([r]\<^sub>! p) \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i ([r']\<^sub>! p))\<close>
+    using K'_map ConE ConI by metis
+  then show ?case
+    by (meson Iff_Iff Iff_Imp Iff_sym PK r)
+next
+  case (Ann s p)
+  then show ?case
+    by simp
+qed
+
+lemma Iff_Ann2:
+  assumes \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! p')\<close>
+  shows \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p')\<close>
+  using assms ConE ConI PImp PR1 PR3 by metis
+
+lemma Iff_reduce: \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! reduce p)\<close>
+proof (induct p)
+  case (Dis p q)
+  then show ?case
+    by (simp add: Iff_Dis)
+next
+  case (Con p q)
+  then show ?case
+    by (simp add: Iff_Con)
+next
+  case (Imp p q)
+  then show ?case
+    by (simp add: Iff_Imp)
+next
+  case (K' i p)
+  have
+    \<open>\<turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i (reduce p))\<close>
+    \<open>\<turnstile>\<^sub>! (K\<^sub>! i (reduce p) \<^bold>\<longrightarrow>\<^sub>! K\<^sub>! i p)\<close>
+    using K' K'_map ConE by fast+
+  then have \<open>\<turnstile>\<^sub>! (K\<^sub>! i p \<^bold>\<longleftrightarrow>\<^sub>! K\<^sub>! i (reduce p))\<close>
+    using ConI by blast
+  then show ?case
+    by simp
+next
+  case (Ann r p)
+  have \<open>\<turnstile>\<^sub>! ([reduce r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p))\<close>
+    using Iff_reduce' static_reduce by blast
+  moreover have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [reduce r]\<^sub>! reduce p)\<close>
+    using Ann(1) Iff_Ann1 static_reduce by blast
+  ultimately have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p))\<close>
+    using Iff_Iff Iff_sym by blast
+  moreover have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! reduce p \<^bold>\<longleftrightarrow>\<^sub>! [r]\<^sub>! p)\<close>
+    by (meson Ann(2) static_reduce Iff_Ann2 Iff_sym)
+  ultimately have \<open>\<turnstile>\<^sub>! ([r]\<^sub>! p \<^bold>\<longleftrightarrow>\<^sub>! reduce' (reduce r) (reduce p))\<close>
+    using Iff_Iff by blast
+  then show ?case
+    by simp
+qed (simp_all add: PA1)
+
+theorem completeness:
+  assumes \<open>\<forall>(M :: ('i :: countable, 'i fm set) kripke) w. M, w \<Turnstile>\<^sub>! p\<close>
+  shows \<open>\<turnstile>\<^sub>! p\<close>
+proof -
+  have \<open>\<forall>(M :: ('i :: countable, 'i fm set) kripke) w. M, w \<Turnstile>\<^sub>! reduce p\<close>
+    using assms reduce_semantics by fast
+  moreover have \<open>static (reduce p)\<close>
+    using static_reduce by fast
+  ultimately have \<open>\<turnstile>\<^sub>! reduce p\<close>
+    using static_completeness by blast
+  moreover have \<open>\<turnstile>\<^sub>! (p \<^bold>\<longleftrightarrow>\<^sub>! reduce p)\<close>
+    using Iff_reduce by blast
+  ultimately show ?thesis
+    using ConE(2) PR1 by blast
+qed
+
+end
diff --git a/thys/Public_Announcement_Logic/ROOT b/thys/Public_Announcement_Logic/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Public_Announcement_Logic/ROOT
@@ -0,0 +1,9 @@
+chapter AFP
+
+session Public_Announcement_Logic (AFP) = "Epistemic_Logic" +
+  options [timeout = 300]
+  theories
+    PAL
+  document_files
+    "root.tex"
+    "root.bib"
diff --git a/thys/Public_Announcement_Logic/document/root.bib b/thys/Public_Announcement_Logic/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Public_Announcement_Logic/document/root.bib
@@ -0,0 +1,12 @@
+@article{WangC13,
+  author  = {Yanjing Wang and
+               Qinxiang Cao},
+  title   = {On axiomatizations of public announcement logic},
+  journal = {Synthese},
+  volume  = {190},
+  number  = {Supplement-1},
+  pages   = {103--134},
+  year    = {2013},
+  doi     = {10.1007/s11229-012-0233-5}
+}
+
diff --git a/thys/Public_Announcement_Logic/document/root.tex b/thys/Public_Announcement_Logic/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Public_Announcement_Logic/document/root.tex
@@ -0,0 +1,66 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{Public Announcement Logic}
+\author{Asta Halkjær From}
+\maketitle
+
+\begin{abstract}
+  This work is a formalization of public announcement logic with countably many agents.
+  It includes proofs of soundness and completeness for a variant of the axiom system PA + DIST! + NEC!~\cite{WangC13}. The completeness proof builds on the Epistemic Logic theory.
+\end{abstract}
+
+\tableofcontents
+
+\newpage
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,606 +1,606 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
+CSP_RefTK
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
-CSP_RefTK
 DFS_Framework
+DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
-DOM_Components
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
-IMP_Compiler
 IMP2
 IMP2_Binary_Heap
+IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
+IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
-IsaGeoCoq
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
-Knuth_Bendix_Order
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
+Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
-Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
+Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
-Shadow_DOM
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
+Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL