diff --git a/thys/SimplifiedOntologicalArgument/DisableKodkodScala.thy b/thys/SimplifiedOntologicalArgument/DisableKodkodScala.thy
deleted file mode 100644
--- a/thys/SimplifiedOntologicalArgument/DisableKodkodScala.thy
+++ /dev/null
@@ -1,14 +0,0 @@
-theory DisableKodkodScala
-  imports Main
-begin
-
-text \<open>Some of the nitpick invocation within this AFP entry do not work,
-  if "Kodkod Scala" is enabled, i.e., if the box under 
-  Plugin Options — Isabelle — General — Miscelleaneous Tools — Kodkod Scala 
-  is activated. Therefore, in this theory we explicitly disable this configuration option.\<close>
-
-ML \<open>
-  Options.default_put_bool \<^system_option>\<open>kodkod_scala\<close> false
-\<close>
-
-end
\ No newline at end of file
diff --git a/thys/SimplifiedOntologicalArgument/SimpleVariant.thy b/thys/SimplifiedOntologicalArgument/SimpleVariant.thy
--- a/thys/SimplifiedOntologicalArgument/SimpleVariant.thy
+++ b/thys/SimplifiedOntologicalArgument/SimpleVariant.thy
@@ -1,42 +1,41 @@
 subsection\<open>Simplified Variant (Fig.~6 in \cite{C85})\<close>
 
 theory SimpleVariant imports 
   HOML 
   MFilter 
   BaseDefs
-  DisableKodkodScala
 begin
 text\<open>Axiom's of new, simplified variant.\<close>
 axiomatization where 
   A1': "\<lfloor>\<^bold>\<not>(\<P>(\<lambda>x.(x\<^bold>\<noteq>x)))\<rfloor>" and 
   A2': "\<lfloor>\<^bold>\<forall>X Y.(((\<P> X) \<^bold>\<and> ((X\<^bold>\<sqsubseteq>Y) \<^bold>\<or> (X\<Rrightarrow>Y))) \<^bold>\<rightarrow> (\<P> Y))\<rfloor>" and
   A3:  "\<lfloor>\<^bold>\<forall>\<Z>.((\<P>\<o>\<s> \<Z>) \<^bold>\<rightarrow> (\<^bold>\<forall>X.((X\<Sqinter>\<Z>) \<^bold>\<rightarrow> (\<P> X))))\<rfloor>" 
 
 lemma T2: "\<lfloor>\<P> \<G>\<rfloor>" by (metis A3 G_def) \<comment>\<open>From A3\<close>
 lemma L1: "\<lfloor>\<P>(\<lambda>x.(x\<^bold>=x))\<rfloor>" by (metis A2' A3) 
 
 text\<open>Necessary existence of a Godlike entity.\<close> 
 theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"  \<comment>\<open>Proof found by sledgehammer\<close>
 proof -
   have T1: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E X))\<rfloor>" by (metis A1' A2') 
   have T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using T1 T2 by simp
   have T5: "\<lfloor>(\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" by (metis A1' A2' T2)
   thus ?thesis using T3 by blast qed
 
 lemma True nitpick[satisfy] oops \<comment>\<open>Consistency: model found\<close>
 
 text\<open>Modal collapse and monotheism: not implied.\<close>
 lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>" nitpick oops \<comment>\<open>Countermodel\<close>
 lemma MT: "\<lfloor>\<^bold>\<forall>x y.(((\<G> x) \<^bold>\<and> (\<G> y)) \<^bold>\<rightarrow> (x\<^bold>=y))\<rfloor>" 
   nitpick oops \<comment>\<open>Countermodel.\<close>
 
 text\<open>Gödel's A1, A4, A5: not implied anymore.\<close>
 lemma A1: "\<lfloor>\<^bold>\<forall>X.((\<^bold>\<not>(\<P> X))\<^bold>\<leftrightarrow>(\<P>(\<^bold>\<rightharpoondown>X)))\<rfloor>" nitpick oops \<comment>\<open>Countermodel\<close>
 lemma A4: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<box>(\<P> X))\<rfloor>" nitpick oops \<comment>\<open>Countermodel\<close>
 lemma A5: "\<lfloor>\<P> \<N>\<E>\<rfloor>" nitpick oops \<comment>\<open>Countermodel\<close>
 
 text\<open>Checking filter and ultrafilter properties.\<close> 
 theorem F1: "\<lfloor>Filter \<P>\<rfloor>" oops \<comment>\<open>Proof found by sledgehammer, but reconstruction timeout\<close>
 theorem U1: "\<lfloor>UFilter \<P>\<rfloor>" nitpick oops  \<comment>\<open>Countermodel\<close>
 end
 
diff --git a/thys/SimplifiedOntologicalArgument/SimpleVariantHF.thy b/thys/SimplifiedOntologicalArgument/SimpleVariantHF.thy
--- a/thys/SimplifiedOntologicalArgument/SimpleVariantHF.thy
+++ b/thys/SimplifiedOntologicalArgument/SimpleVariantHF.thy
@@ -1,39 +1,38 @@
 subsection\<open>Hauptfiltervariant (Fig.~10 in \cite{C85})\<close>
 
 theory SimpleVariantHF imports
   HOML 
   MFilter 
   BaseDefs
-  DisableKodkodScala
 begin
 text\<open>Definition: Set of supersets of \<open>X\<close>, we call this \<open>\<H>\<F> X\<close>.\<close>
 abbreviation HF::"\<gamma>\<Rightarrow>(\<gamma>\<Rightarrow>\<sigma>)"  where "HF X \<equiv> \<lambda>Y.(X\<^bold>\<sqsubseteq>Y)"
 
 text\<open>Postulate: \<open>\<H>\<F> \<G>\<close> is a filter; i.e., Hauptfilter of \<open>\<G>\<close>.\<close> 
 axiomatization where F1: "\<lfloor>Filter (HF \<G>)\<rfloor>" 
 
 text\<open>Necessary existence of a Godlike entity.\<close> 
 theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using F1 by auto \<comment>\<open>Proof found\<close>
 
 theorem T6again: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"  
 proof -
  have T3': "\<lfloor>\<^bold>\<exists>\<^sup>E \<G>\<rfloor>" using F1 by auto
  have T6:  "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using T3' by blast 
  thus ?thesis by simp qed
 
 text\<open>Possible existence of Godlike entity not implied.\<close>
 lemma T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" nitpick oops  \<comment>\<open>Countermodel\<close>
 
 text\<open>Axiom T enforces possible existence of Godlike entity.\<close>
 axiomatization 
 lemma T3: assumes T: "\<lfloor>\<^bold>\<forall>\<phi>.((\<^bold>\<box>\<phi>) \<^bold>\<rightarrow> \<phi>)\<rfloor>"
           shows "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using F1 T by auto
 
 lemma True nitpick[satisfy] oops \<comment>\<open>Consistency: model found\<close>
 
 text\<open>Modal collapse: not implied anymore.\<close>
 lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>" nitpick oops  \<comment>\<open>Countermodel\<close>
 lemma MT: "\<lfloor>\<^bold>\<forall>x y.(((\<G> x) \<^bold>\<and> (\<G> y)) \<^bold>\<rightarrow> (x\<^bold>=y))\<rfloor>" 
           nitpick oops \<comment>\<open>Countermodel\<close>
 end
 
diff --git a/thys/SimplifiedOntologicalArgument/SimpleVariantPG.thy b/thys/SimplifiedOntologicalArgument/SimpleVariantPG.thy
--- a/thys/SimplifiedOntologicalArgument/SimpleVariantPG.thy
+++ b/thys/SimplifiedOntologicalArgument/SimpleVariantPG.thy
@@ -1,28 +1,27 @@
 subsection\<open>Simplified Variant with Axiom T2 (Fig.~7 in \cite{C85})\<close>
 
 theory SimpleVariantPG imports 
   HOML 
   MFilter 
   BaseDefs
-  DisableKodkodScala
 begin
 text\<open>Axiom's of simplified variant with A3 replaced.\<close> 
 axiomatization where 
   A1': "\<lfloor>\<^bold>\<not>(\<P>(\<lambda>x.(x\<^bold>\<noteq>x)))\<rfloor>" and
   A2': "\<lfloor>\<^bold>\<forall>X Y.(((\<P> X) \<^bold>\<and> ((X\<^bold>\<sqsubseteq>Y)\<^bold>\<or>(X\<Rrightarrow>Y))) \<^bold>\<rightarrow> (\<P> Y))\<rfloor>" and
   T2:  "\<lfloor>\<P> \<G>\<rfloor>"
 
 text\<open>Necessary existence of a Godlike entity.\<close> 
 theorem T6:  "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"  \<comment>\<open>Proof found by sledgehammer\<close>
 proof -
   have T1: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E X))\<rfloor>" by (metis A1' A2') 
   have T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using T1 T2 by simp
   have T5: "\<lfloor>(\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" by (metis A1' A2' T2)
   thus ?thesis using T3 by blast qed
 
 lemma True nitpick[satisfy] oops  \<comment>\<open>Consistency: model found\<close>
 
 text\<open>Modal collapse and Monotheism: not implied.\<close>
 lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>" nitpick oops  \<comment>\<open>Countermodel\<close>
 lemma MT: "\<lfloor>\<^bold>\<forall>x y.(((\<G> x)\<^bold>\<and>(\<G> y))\<^bold>\<rightarrow>(x\<^bold>=y))\<rfloor>" nitpick oops  \<comment>\<open>Countermodel\<close>
 end
diff --git a/thys/SimplifiedOntologicalArgument/SimplifiedOntologicalArgument.thy b/thys/SimplifiedOntologicalArgument/SimplifiedOntologicalArgument.thy
--- a/thys/SimplifiedOntologicalArgument/SimplifiedOntologicalArgument.thy
+++ b/thys/SimplifiedOntologicalArgument/SimplifiedOntologicalArgument.thy
@@ -1,72 +1,71 @@
 section \<open>Selected Simplified Ontological Argument \label{sec:selected}\<close>
 
 theory SimplifiedOntologicalArgument imports 
   HOML
-  DisableKodkodScala
 begin
 text \<open>Positive properties:\<close>
 consts posProp::"\<gamma>\<Rightarrow>\<sigma>" ("\<P>")
 
 text \<open>An entity x is God-like if it possesses all positive properties.\<close>
 definition G ("\<G>") where "\<G>(x) \<equiv> \<^bold>\<forall>\<Phi>.(\<P>(\<Phi>) \<^bold>\<rightarrow> \<Phi>(x))"
 
 text \<open>The axiom's of the simplified variant are presented next; these axioms are further motivated in \cite{C85,J52}).\<close> 
 text \<open>Self-difference is not a positive property (possible alternative: 
       the empty property is not a positive property).\<close>
 axiomatization where CORO1: "\<lfloor>\<^bold>\<not>(\<P>(\<lambda>x.(x\<^bold>\<noteq>x)))\<rfloor>" 
 text \<open>A property entailed by a positive property is positive.\<close>
 axiomatization where CORO2: "\<lfloor>\<^bold>\<forall>\<Phi> \<Psi>. \<P>(\<Phi>) \<^bold>\<and> (\<^bold>\<forall>x. \<Phi>(x) \<^bold>\<rightarrow> \<Psi>(x)) \<^bold>\<rightarrow> \<P>(\<Psi>)\<rfloor>" 
 text \<open>Being Godlike is a positive property.\<close>
 axiomatization where AXIOM3: "\<lfloor>\<P> \<G>\<rfloor>" 
 
 subsection\<open>Verifying the Selected Simplified Ontological Argument (version 1)\<close>
 
 text \<open>The existence of a non-exemplified positive property implies that self-difference 
       (or, alternatively, the empty property) is a positive property.\<close>
 lemma LEMMA1: "\<lfloor>(\<^bold>\<exists>\<Phi>.(\<P>(\<Phi>) \<^bold>\<and> \<^bold>\<not>(\<^bold>\<exists>x. \<Phi>(x)))) \<^bold>\<rightarrow> \<P>(\<lambda>x.(x\<^bold>\<noteq>x))\<rfloor>" 
   using CORO2 by meson 
 text \<open>A non-exemplified positive property does not exist.\<close>
 lemma LEMMA2: "\<lfloor>\<^bold>\<not>(\<^bold>\<exists>\<Phi>.(\<P>(\<Phi>) \<^bold>\<and> \<^bold>\<not>(\<^bold>\<exists>x. \<Phi>(x))))\<rfloor>" 
   using CORO1 LEMMA1 by blast
 text \<open>Positive properties are exemplified.\<close>
 lemma LEMMA3: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<P>(\<Phi>) \<^bold>\<rightarrow> (\<^bold>\<exists>x. \<Phi>(x)))\<rfloor>" 
   using LEMMA2 by blast
 text \<open>There exists a God-like entity.\<close>
 theorem THEOREM3': "\<lfloor>\<^bold>\<exists>x. \<G>(x)\<rfloor>" 
   using AXIOM3 LEMMA3 by auto
 text \<open>Necessarily, there exists a God-like entity.\<close>
 theorem THEOREM3: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>x. \<G>(x))\<rfloor>" 
   using THEOREM3' by simp
 text \<open>However, the possible existence of Godlike entity is not implied.\<close>
 theorem CORO: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>x. \<G>(x))\<rfloor>" 
   nitpick oops (*Countermodel*)
 
 subsection\<open>Verifying the Selected Simplified Ontological Argument (version 2)\<close>
 
 text \<open>We switch to logic T.\<close>
 axiomatization where T: "\<lfloor>\<^bold>\<forall>\<phi>. \<^bold>\<box>\<phi> \<^bold>\<rightarrow> \<phi>\<rfloor>" 
 lemma T': "\<lfloor>\<^bold>\<forall>\<phi>. \<phi> \<^bold>\<rightarrow> \<^bold>\<diamond>\<phi>\<rfloor>" using T by metis
 text \<open>Positive properties are possibly exemplified.\<close>
 theorem THEOREM1: "\<lfloor>\<^bold>\<forall>\<Phi>. \<P>(\<Phi>) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>x. \<Phi>(x))\<rfloor>" 
   using CORO1 CORO2 T' by metis
 text \<open>Possibly there exists a God-like entity.\<close>
 theorem CORO: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>x. \<G>(x))\<rfloor>" 
   using AXIOM3 THEOREM1 by auto
 text \<open>The possible existence of a God-like entity impplies the necessary  existence of a God-like entity.\<close>
 theorem THEOREM2: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>x. \<G>(x)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>x. \<G>(x))\<rfloor>" 
   using AXIOM3 CORO1 CORO2 by metis
 text \<open>Necessarily, there exists a God-like entity.\<close>
 theorem THEO3: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>x. \<G>(x))\<rfloor>" 
   using CORO THEOREM2 by blast 
 text \<open>There exists a God-like entity.\<close>
 theorem THEO3': "\<lfloor>\<^bold>\<exists>x. \<G>(x)\<rfloor>" 
   using T THEO3 by metis
 
 text \<open>Modal collapse is not implied; nitpick reports a countermodel.\<close>
 
 lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>. \<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>\<rfloor>" nitpick oops
 
 text \<open>Consistency of the theory; nitpick reports a model.\<close>
 lemma True nitpick[satisfy] oops (*Model found*)
 end
 
diff --git a/thys/SimplifiedOntologicalArgument/UFilterVariant.thy b/thys/SimplifiedOntologicalArgument/UFilterVariant.thy
--- a/thys/SimplifiedOntologicalArgument/UFilterVariant.thy
+++ b/thys/SimplifiedOntologicalArgument/UFilterVariant.thy
@@ -1,46 +1,45 @@
 subsection\<open>Ultrafilter Variant (Fig.~5 in \cite{C85})\<close>
 
 theory UFilterVariant imports 
   HOML 
   MFilter 
   BaseDefs
-  DisableKodkodScala
 begin
 text\<open>Axiom's of ultrafilter variant.\<close> 
 axiomatization where 
   U1: "\<lfloor>UFilter \<P>\<rfloor>" and
   A2: "\<lfloor>\<^bold>\<forall>X Y.(((\<P> X) \<^bold>\<and> (X\<Rrightarrow>Y)) \<^bold>\<rightarrow> (\<P> Y))\<rfloor>" and
   A3: "\<lfloor>\<^bold>\<forall>\<Z>.((\<P>\<o>\<s> \<Z>) \<^bold>\<rightarrow> (\<^bold>\<forall>X.((X\<Sqinter>\<Z>) \<^bold>\<rightarrow> (\<P> X))))\<rfloor>" 
 
 text\<open>Necessary existence of a Godlike entity.\<close>  
 theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" \<comment>\<open>Proof also found by sledgehammer\<close>
 proof -
   have T1: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E X))\<rfloor>" by (metis A2 U1) 
   have T2: "\<lfloor>\<P> \<G>\<rfloor>" by (metis A3 G_def)
   have T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" using T1 T2 by simp
   have T5: "\<lfloor>(\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>" by (metis A2 G_def T2 U1)
   thus ?thesis using T3 by blast qed
 
 text\<open>Checking for consistency.\<close>  
 lemma True nitpick[satisfy] oops  \<comment>\<open>Model found\<close>
 
 text\<open>Checking for modal collapse.\<close>
 lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>" nitpick oops \<comment>\<open>Countermodel\<close>
 end
 
 
 
 (*
  definition ess ("\<E>") where "\<E> Y x \<equiv> Y x \<^bold>\<and> (\<^bold>\<forall>Z.(Z x \<^bold>\<rightarrow> (Y\<Rrightarrow>Z)))" 
  definition NE ("NE") where "NE x \<equiv> \<lambda>w.((\<^bold>\<forall>Y.(\<E> Y x \<^bold>\<rightarrow> \<^bold>\<box>\<^bold>\<exists>\<^sup>E Y)) w)"
  consts Godlike::\<gamma> UltraFilter::"(\<gamma>\<Rightarrow>\<sigma>)\<Rightarrow>\<sigma>" NeEx::\<gamma>
  axiomatization where 
   1: "Godlike = G" and 
   2: "UltraFilter = Ultrafilter" and
   3: "NeEx = NE"
  lemma True nitpick[satisfy] oops 
  lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>. \<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>\<rfloor>" nitpick[format=8] oops (*Countermodel*)
  lemma A1: "\<lfloor>\<^bold>\<forall>X. \<^bold>\<not>(\<P> X) \<^bold>\<leftrightarrow> \<P>(\<^bold>\<rightharpoondown>X)\<rfloor>" using U1 by fastforce
  lemma A4: "\<lfloor>(\<P> X \<^bold>\<rightarrow> \<^bold>\<box>(\<P> X))\<rfloor>" nitpick [format=4] oops (*Countermodel*)
  lemma A5: "\<lfloor>\<P> NE\<rfloor>" nitpick oops (*Countermodel*)
 *)
\ No newline at end of file