diff --git a/thys/Goedel_HFSet_Semantic/Instance.thy b/thys/Goedel_HFSet_Semantic/Instance.thy
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_HFSet_Semantic/Instance.thy
@@ -0,0 +1,465 @@
+section \<open>The Instantiation\<close>
+
+(*<*)
+theory Instance
+  imports Goedel_Incompleteness.Abstract_Second_Goedel
+    Incompleteness.Quote Incompleteness.Goedel_I
+begin
+(*>*)
+
+definition "Fvars t = {a :: name. \<not> atom a \<sharp> t}"
+
+lemma Fvars_tm_simps[simp]:
+  "Fvars Zero = {}"
+  "Fvars (Var a) = {a}"
+  "Fvars (Eats x y) = Fvars x \<union> Fvars y"
+  by (auto simp: Fvars_def fresh_at_base(2))
+
+lemma finite_Fvars_tm[simp]:
+  fixes t :: tm
+  shows "finite (Fvars t)"
+  by (induct t rule: tm.induct) auto
+
+lemma Fvars_fm_simps[simp]:
+  "Fvars (x IN y) = Fvars x \<union> Fvars y"
+  "Fvars (x EQ y) = Fvars x \<union> Fvars y"
+  "Fvars (A OR B) = Fvars A \<union> Fvars B"
+  "Fvars (A AND B) = Fvars A \<union> Fvars B"
+  "Fvars (A IMP B) = Fvars A \<union> Fvars B"
+  "Fvars Fls = {}"
+  "Fvars (Neg A) = Fvars A"
+  "Fvars (Ex a A) = Fvars A - {a}"
+  "Fvars (All a A) = Fvars A - {a}"
+  by (auto simp: Fvars_def fresh_at_base(2))
+
+lemma finite_Fvars_fm[simp]:
+  fixes A :: fm
+  shows "finite (Fvars A)"
+  by (induct A rule: fm.induct) auto
+
+lemma subst_tm_subst_tm[simp]:
+  "x \<noteq> y \<Longrightarrow> atom x \<sharp> u \<Longrightarrow> subst y u (subst x t v) = subst x (subst y u t) (subst y u v)"
+  by (induct v rule: tm.induct) auto
+
+lemma subst_fm_subst_fm[simp]:
+  "x \<noteq> y \<Longrightarrow> atom x \<sharp> u \<Longrightarrow> (A(x::=t))(y::=u) = (A(y::=u))(x::=subst y u t)"
+  by (nominal_induct A avoiding: x t y u rule: fm.strong_induct) auto
+
+lemma Fvars_ground_aux: "Fvars t \<subseteq> B \<Longrightarrow> ground_aux t (atom ` B)"
+  by (induct t rule: tm.induct) auto
+
+lemma ground_Fvars: "ground t \<longleftrightarrow> Fvars t = {}"
+  apply (rule iffI)
+   apply (auto simp only: Fvars_def ground_fresh) []
+  apply (auto intro: Fvars_ground_aux[of t "{}", simplified])
+  done
+
+lemma Fvars_ground_fm_aux: "Fvars A \<subseteq> B \<Longrightarrow> ground_fm_aux A (atom ` B)"
+  apply (induct A arbitrary: B rule: fm.induct)
+      apply (auto simp: Diff_subset_conv Fvars_ground_aux)
+  apply (drule meta_spec, drule meta_mp, assumption)
+  apply auto
+  done
+
+lemma ground_fm_Fvars: "ground_fm A \<longleftrightarrow> Fvars A = {}"
+  apply (rule iffI)
+   apply (auto simp only: Fvars_def ground_fresh) []
+  apply (auto intro: Fvars_ground_fm_aux[of A "{}", simplified])
+  done
+
+interpretation Generic_Syntax where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  apply unfold_locales
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal for t by (induct t rule: tm.induct) auto
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal unfolding Fvars_def fresh_subst_fm_if by auto
+  subgoal unfolding Fvars_def by auto
+  subgoal unfolding Fvars_def by simp
+  subgoal by simp
+  subgoal unfolding Fvars_def by simp
+  done
+
+lemma coding_tm_Fvars_empty[simp]: "coding_tm t \<Longrightarrow> Fvars t = {}"
+  by (induct t rule: coding_tm.induct) (auto simp: Fvars_def)
+
+lemma Fvars_empty_ground[simp]: "Fvars t = {} \<Longrightarrow> ground t"
+  by (induct t rule: tm.induct) auto
+
+interpretation Syntax_with_Numerals where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  apply unfold_locales
+  subgoal by (auto intro!: exI[of _ Zero])
+  subgoal by simp
+  subgoal by (simp add: ground_Fvars)
+  done
+
+declare FvarsT_num[simp del]
+
+interpretation Deduct2_with_False where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  apply unfold_locales
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal unfolding Fvars_def by simp
+  subgoal unfolding Fvars_def by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal using MP_null by blast
+  subgoal by blast
+  subgoal for A B C
+    apply (rule Imp_I)+
+    apply (rule MP_same[of _ B])
+     apply (rule MP_same[of _ C])
+      apply (auto intro: Neg_D)
+    done
+  subgoal by blast
+  subgoal by blast
+  subgoal by blast
+  subgoal unfolding Fvars_def by (auto intro: MP_null)
+  subgoal unfolding Fvars_def by (auto intro: MP_null)
+  subgoal by (auto intro: All_D)
+  subgoal by (auto intro: Ex_I)
+  subgoal by simp
+  subgoal by (metis Conj_E2 Iff_def Imp_I Var_Eq_subst_Iff)
+  subgoal by blast
+  subgoal by simp
+  done
+
+interpretation HBL1 where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  and enc = "quot"
+  and P = "PfP (Var xx)"
+  apply unfold_locales
+  subgoal by (simp add: quot_fm_coding)
+  subgoal by simp
+  subgoal unfolding Fvars_def by (auto simp: fresh_at_base(2))
+  subgoal by (auto simp: proved_imp_proved_PfP)
+  done
+
+interpretation Goedel_Form where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  and enc = "quot"
+  and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
+  and P = "PfP (Var xx)"
+  apply unfold_locales
+  subgoal by simp
+  subgoal unfolding Fvars_def by (auto simp: fresh_at_base(2))
+  subgoal
+    unfolding Let_def
+    by (subst psubst_eq_rawpsubst2)
+      (auto simp: quot_fm_coding prove_KRP Fvars_def)
+  subgoal
+    unfolding Let_def
+    by (subst (1 2) psubst_eq_rawpsubst2)
+      (auto simp: quot_fm_coding KRP_unique[THEN Sym] Fvars_def)
+  done
+
+interpretation g2: Goedel_Second_Assumptions where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  and enc = "quot"
+  and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
+  and P = "PfP (Var xx)"
+  apply unfold_locales
+  subgoal by (auto simp: PP_def intro: PfP_implies_ModPon_PfP_quot)
+  subgoal by (auto simp: PP_def quot_fm_coding Provability)
+  done
+
+theorem Goedel_II: "\<not> {} \<turnstile> Fls \<Longrightarrow> \<not> {} \<turnstile> neg (PfP \<guillemotleft>Fls\<guillemotright>)"
+  by (rule g2.goedel_second[unfolded consistent_def PP_def PfP_subst subst.simps simp_thms if_True])
+
+lemma ground_fm_PrfP[simp]:
+  "ground_fm (PrfP s k t) \<longleftrightarrow> ground s \<and> ground k \<and> ground t"
+  by (auto simp add: ground_aux_def ground_fm_aux_def supp_conv_fresh)
+
+
+lemma Fvars_HPair[simp]: "Fvars (HPair t u) = Fvars t \<union> Fvars u"
+  unfolding Fvars_def
+  by auto
+
+lemma ground_HPair[simp]: "ground (HPair t u) \<longleftrightarrow> ground t \<and> ground u"
+  unfolding ground_Fvars
+  by auto
+
+interpretation dwfd: Deduct2_with_False_Disj where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and dsj = "(OR)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  apply unfold_locales
+  subgoal by simp
+  subgoal by simp
+  subgoal by simp
+  subgoal by (auto intro: Disj_I1)
+  subgoal by (auto intro: Disj_I2)
+  subgoal by (auto intro: ContraAssume)
+  subgoal by simp
+  done
+
+interpretation Minimal_Truth_Soundness where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and dsj = "(OR)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and isTrue = "eval_fm e0"
+  apply unfold_locales
+  subgoal by (auto simp: Fls_def)
+  subgoal by simp
+  subgoal by (auto simp only: ex_eval_fm_iff_exists_tm eval_fm.simps(4) subst_fm.simps)
+  subgoal by (auto simp only: ex_eval_fm_iff_exists_tm)
+  subgoal by (simp add: neg_def)
+  subgoal by (auto dest: hfthm_sound)
+  done
+
+lemma neg_Neg:
+  "{} \<turnstile> neg \<phi> IFF Neg \<phi>"
+  unfolding neg_def
+  by (auto simp: Fls_def intro: ContraAssume)
+
+
+lemma ground_aux_mono: "A \<subseteq> B \<Longrightarrow> ground_aux t A \<Longrightarrow> ground_aux t B"
+  unfolding ground_aux_def by auto
+
+interpretation g1: Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and dsj = "(OR)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  and enc = "quot"
+  and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
+  and P = "PfP (Var xx)"
+  and isTrue = "eval_fm e0"
+  and Pf = "Ex xx' (Ex yy' (Var yy EQ HPair (Var xx') (Var yy') AND PrfP (Var xx') (Var yy') (Var xx)))"
+  apply unfold_locales
+  subgoal by simp
+  subgoal unfolding Fvars_def by (auto simp: fresh_at_base(2))
+  subgoal for \<phi>
+    unfolding Let_def
+    supply PfP.simps[simp del]
+    apply (subst psubst_eq_rawpsubst2) apply (simp_all add: PfP.simps[of yy' xx' "quot \<phi>", simplified])
+    apply (auto simp: eqv_def)
+     apply (rule Ex_I[of _ _ _ "HPair (Var xx') (Var yy')"])
+     apply (subst subst_fm_Ex_with_renaming[of xx _ xx' yy]; (auto simp: Conj_eqvt))
+     apply (subst subst_fm_Ex_with_renaming[of zz _ yy' yy]; (auto simp: Conj_eqvt HPair_eqvt PrfP.eqvt))
+     apply (rule Ex_I[of _ _ _ "(Var xx')"]; auto)
+     apply (rule Ex_I[of _ _ _ "(Var yy')"]; auto)
+     apply (rule Ex_I[of _ _ _ "(Var yy')"]; auto)
+    apply (rule Ex_I[of _ _ _ "(Var xx')"]; auto)
+    done
+  subgoal
+    by (auto simp: PP_def proved_iff_proved_PfP[symmetric])
+  subgoal for n \<phi>
+    unfolding Let_def
+    apply (subst (1 2) psubst_eq_rawpsubst2)
+           apply (simp_all add: ground_Fvars)
+    apply (rule impI)
+    apply (rule Sigma_fm_imp_thm)
+      apply (auto simp: ground_Fvars[symmetric] elim: ground_aux_mono[OF empty_subsetI])
+     apply (auto simp: ground_aux_def ground_fm_aux_def supp_conv_fresh fresh_at_base Fvars_def)
+    done
+  subgoal for \<phi>
+    apply (rule NegNeg_D)
+    apply (auto simp: PP_def dest!: Iff_MP_same[OF neg_Neg] Iff_MP_same[OF Neg_cong[OF neg_Neg]])
+    done
+  done
+
+theorem Goedel_I: "\<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> eval_fm e0 \<phi>"
+  by (meson Iff_MP2_same g1.recover_proofs.goedel_first_classic_strong[OF consistent] neg_Neg)
+
+text \<open>
+The following interpretation is redundant, because
+@{locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical} (interpreted above)
+is a sublocale of @{locale Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP}.
+However, the latter requires less infrastructure (no Pf formula).
+
+The definition of isTrue prevents Isabelle from noticing that the locale has already been
+interpreted via the above g1 interpretation of
+@{locale Goedel_Form_Minimal_Truth_Soundness_HBL1iff_prv_Compl_Pf_Classical}.
+\<close>
+
+definition isTrue where
+  "isTrue = eval_fm e0"
+
+interpretation g1': Goedel_Form_Classical_HBL1_rev_prv_Minimal_Truth_Soundness_TIP where
+      var = "UNIV :: name set"
+  and trm = "UNIV :: tm set"
+  and fmla = "UNIV :: fm set"
+  and num = "{t. ground t}"
+  and Var = Var
+  and FvarsT = Fvars
+  and substT = "\<lambda>t u x. subst x u t"
+  and Fvars = Fvars
+  and subst = "\<lambda>A u x. subst_fm A x u"
+  and eql = "(EQ)"
+  and cnj = "(AND)"
+  and dsj = "(OR)"
+  and imp = "(IMP)"
+  and all = "All"
+  and exi = "Ex"
+  and fls = "Fls"
+  and prv = "(\<turnstile>) {}"
+  and bprv = "(\<turnstile>) {}"
+  and enc = "quot"
+  and S = "KRP (quot (Var xx)) (Var xx) (Var yy)"
+  and P = "PfP (Var xx)"
+  and isTrue = "isTrue"
+  apply unfold_locales
+  unfolding isTrue_def
+  subgoal by (auto simp: Fls_def)
+  subgoal by simp
+  subgoal by (auto simp only: ex_eval_fm_iff_exists_tm eval_fm.simps(4) subst_fm.simps)
+  subgoal by (auto simp only: ex_eval_fm_iff_exists_tm)
+  subgoal by (simp add: neg_def)
+  subgoal by (auto dest: hfthm_sound)
+  subgoal by (auto simp: proved_iff_proved_PfP[symmetric] PP_def quot_fm_coding
+        simp del: eval_fm_PfP
+        dest!: Iff_MP_same[OF neg_Neg] Iff_MP_same[OF Neg_cong[OF neg_Neg]] NegNeg_D
+        Sigma_fm_imp_thm[rotated 2])
+  done
+
+theorem Goedel_I': "\<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> isTrue \<phi>"
+  by (meson Iff_MP2_same g1'.goedel_first_classic_strong[OF consistent] neg_Neg)
+
+(*<*)
+end
+(*>*)
diff --git a/thys/Goedel_HFSet_Semantic/ROOT b/thys/Goedel_HFSet_Semantic/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_HFSet_Semantic/ROOT
@@ -0,0 +1,11 @@
+chapter AFP
+
+session Goedel_HFSet_Semantic (AFP) = Goedel_Incompleteness +
+  description \<open>Reproduction of Paulson's Formalization of Incompleteness Theorems\<close>
+  options [timeout = 2400]
+  sessions
+    Incompleteness
+  theories
+    Instance
+  document_files
+    "root.tex"
diff --git a/thys/Goedel_HFSet_Semantic/document/root.tex b/thys/Goedel_HFSet_Semantic/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Goedel_HFSet_Semantic/document/root.tex
@@ -0,0 +1,46 @@
+\documentclass[10pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+\usepackage{a4wide}
+\usepackage[english]{babel}
+\usepackage{eufrak}
+\usepackage{amssymb}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{literal}
+
+
+\begin{document}
+
+\title{From Abstract to Concrete G\"odel's Incompleteness Theorems---Part I}
+\author{Andrei Popescu \and Dmitriy Traytel}
+
+\maketitle
+
+\begin{abstract} We validate an abstract formulation of G\"odel's First and Second Incompleteness Theorems
+from a \href{https://www.isa-afp.org/entries/Goedel_Incompleteness.html}{separate AFP entry} by instantiating
+them to the case of \emph{finite sound extensions of the Hereditarily Finite (HF) Set theory}, i.e., FOL
+theories extending the HF Set theory with a finite set of axioms that are sound in the standard model. The
+concrete results had been previously formalised in an
+\href{https://www.isa-afp.org/entries/Incompleteness.html}{AFP entry by Larry Paulson}; our instantiation
+reuses the infrastructure developed in that entry.
+\end{abstract}
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+\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,558 +1,559 @@
 ADS_Functor
 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
 Banach_Steinhaus
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 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
 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
 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
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 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
 DynamicArchitectures
 Dynamic_Tables
 EFSM_Inference
 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_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_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 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
 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_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 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
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 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
 Mersenne_Primes
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 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
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 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
 Projective_Geometry
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 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
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 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
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 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
 VectorSpace
 VeriComp
 Verified-Prover
 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