# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1605445693 0
# Node ID 00fce84413db8bd806976832638771d571156106
# Parent  b5c23767ddd594f2b42645f7f7cd84c7dad50a3d
trival

diff -r b5c23767ddd5 -r 00fce84413db src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Sun Nov 15 13:06:41 2020 +0000
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Sun Nov 15 13:08:13 2020 +0000
@@ -566,7 +566,7 @@
      in this rule. For example, if \<^term>\<open>e\<close> is constantly \<^term>\<open>True\<close> then 
      \<^term>\<open>assigns_if False e = UNIV\<close> and therefor \<^term>\<open>nrm C2=UNIV\<close>.
      So finally \<^term>\<open>nrm A = nrm C1\<close>. For the break maps this trick 
-     workd too, because the trival break map will map all labels to 
+     workd too, because the trivial break map will map all labels to 
      \<^term>\<open>UNIV\<close>. In the example, if no break occurs in \<^term>\<open>c2\<close> the break
      maps will trivially map to \<^term>\<open>UNIV\<close> and if a break occurs it will map
      to \<^term>\<open>UNIV\<close> too, because \<^term>\<open>assigns_if False e = UNIV\<close>. So
diff -r b5c23767ddd5 -r 00fce84413db src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Nov 15 13:06:41 2020 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Nov 15 13:08:13 2020 +0000
@@ -3131,7 +3131,7 @@
   for p :: "'a::field poly"
   by (cases "p = 0") (auto simp: is_unit_triv is_unit_iff_degree)
 
-lemma is_unit_monom_trival: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
+lemma is_unit_monom_trivial: "is_unit p \<Longrightarrow> monom (coeff p (degree p)) 0 = p"
   for p :: "'a::field poly"
   by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
 
diff -r b5c23767ddd5 -r 00fce84413db src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Nov 15 13:06:41 2020 +0000
+++ b/src/HOL/Divides.thy	Sun Nov 15 13:08:13 2020 +0000
@@ -440,7 +440,7 @@
     by auto
 qed
 
-lemma zmod_trival_iff:
+lemma zmod_trivial_iff:
   fixes i k :: int
   shows "i mod k = i \<longleftrightarrow> k = 0 \<or> 0 \<le> i \<and> i < k \<or> i \<le> 0 \<and> k < i"
 proof -
@@ -488,7 +488,7 @@
       using pos_mod_bound [of l k] apply linarith 
       done
     with \<open>l > 0\<close> have \<open>(k mod l - 1) mod l = k mod l - 1\<close>
-      by (simp add: zmod_trival_iff)
+      by (simp add: zmod_trivial_iff)
     ultimately show ?thesis
       apply (simp only: zmod_zminus1_eq_if)
       apply (simp add: mod_eq_0_iff_dvd algebra_simps mod_simps)
@@ -1240,7 +1240,7 @@
   have \<open>(k + 1) mod 2 ^ n = (k mod 2 ^ n + 1) mod 2 ^ n\<close>
     by (simp add: mod_simps)
   also have \<open>\<dots> = k mod 2 ^ n + 1\<close>
-    using * by (simp add: zmod_trival_iff)
+    using * by (simp add: zmod_trivial_iff)
   finally have \<open>(k + 1) mod 2 ^ n = k mod 2 ^ n + 1\<close> .
   then show ?thesis
     by (simp add: take_bit_eq_mod)
@@ -1259,7 +1259,7 @@
   have \<open>(k - 1) mod 2 ^ n = (k mod 2 ^ n - 1) mod 2 ^ n\<close>
     by (simp add: mod_simps)
   also have \<open>\<dots> = k mod 2 ^ n - 1\<close>
-    by (simp add: zmod_trival_iff)
+    by (simp add: zmod_trivial_iff)
       (use \<open>k mod 2 ^ n < 2 ^ n\<close> * in linarith)
   finally have \<open>(k - 1) mod 2 ^ n = k mod 2 ^ n - 1\<close> .
   then show ?thesis
diff -r b5c23767ddd5 -r 00fce84413db 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)"