src/HOL/Set.thy

--- a/src/HOL/Set.thy	Sun Nov 15 13:06:41 2020 +0000
+++ b/src/HOL/Set.thy	Sun Nov 15 13:08:13 2020 +0000
@@ -383,7 +383,7 @@
   unfolding Bex_def by blast
 
 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<longrightarrow> P)"
-  \<comment> \<open>Trival rewrite rule.\<close>
+  \<comment> \<open>trivial rewrite rule.\<close>
   by (simp add: Ball_def)
 
 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) \<longleftrightarrow> ((\<exists>x. x \<in> A) \<and> P)"