isabelle update_cartouches;

--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sun Dec 05 20:17:17 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Dec 06 12:39:59 2021 +0100
@@ -920,7 +920,7 @@
  assumes "is_unit x"
  shows "infinite {n. x^n dvd y}"
 proof -
- from `is_unit x` have "is_unit (x^n)" for n
+ from \<open>is_unit x\<close> have "is_unit (x^n)" for n
    using is_unit_power_iff by auto
  hence "x^n dvd y" for n
    by auto
@@ -2181,7 +2181,7 @@
    using is_unit_power_iff by simp
  hence "p^k dvd x"
    by auto
- moreover from `is_unit p` have "p^k dvd p^multiplicity p x"
+ moreover from \<open>is_unit p\<close> have "p^k dvd p^multiplicity p x"
    using multiplicity_unit_left is_unit_power_iff by simp
  ultimately show ?thesis by simp
 next
@@ -2194,16 +2194,16 @@
    moreover have "p^k dvd x \<Longrightarrow> k = 0"
    proof (rule ccontr)
      assume "p^k dvd x" and "k \<noteq> 0"
-     with `p = 0` have "p^k = 0" by auto
-     with `p^k dvd x` have "0 dvd x" by auto
+     with \<open>p = 0\<close> have "p^k = 0" by auto
+     with \<open>p^k dvd x\<close> have "0 dvd x" by auto
      hence "x = 0" by auto
-     with `x \<noteq> 0` show False by auto
+     with \<open>x \<noteq> 0\<close> show False by auto
    qed
    ultimately show ?thesis
-     by (auto simp add: is_unit_power_iff `\<not> is_unit p`)
+     by (auto simp add: is_unit_power_iff \<open>\<not> is_unit p\<close>)
  next
    case False
-   with `x \<noteq> 0` `\<not> is_unit p` show ?thesis
+   with \<open>x \<noteq> 0\<close> \<open>\<not> is_unit p\<close> show ?thesis
      by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power)
  qed
 qed

--- a/src/HOL/Equiv_Relations.thy	Sun Dec 05 20:17:17 2021 +0100
+++ b/src/HOL/Equiv_Relations.thy	Mon Dec 06 12:39:59 2021 +0100
@@ -368,7 +368,7 @@
   have eqv: "equiv S ?r"
     unfolding relation_of_def by (auto intro: comp_equivI)
   have finite: "C \<in> S//?r \<Longrightarrow> finite C" for C
-    by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]])
+    by (fact finite_equiv_class[OF \<open>finite S\<close> equiv_type[OF \<open>equiv S ?r\<close>]])
   have disjoint: "A \<in> S//?r \<Longrightarrow> B \<in> S//?r \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}" for A B
     using eqv quotient_disj by blast
 

--- a/src/HOL/Set_Interval.thy	Sun Dec 05 20:17:17 2021 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Dec 06 12:39:59 2021 +0100
@@ -1581,7 +1581,7 @@
   assume "finite S" and "\<not> Suc (Max S) \<ge> card S"
   then have "Suc (Max S) < card S"
     by simp
-  with `finite S` have "S \<subseteq> {0..Max S}"
+  with \<open>finite S\<close> have "S \<subseteq> {0..Max S}"
     by auto
   hence "card S \<le> card {0..Max S}"
     by (intro card_mono; auto)
@@ -2110,14 +2110,14 @@
     let ?S' = "S - {Max S}"
     from Suc have "Max S \<in> S" by (auto intro: Max_in)
     hence cards: "card S = Suc (card ?S')"
-      using `finite S` by (intro card.remove; auto)
+      using \<open>finite S\<close> by (intro card.remove; auto)
     hence "\<Sum> {0..<card ?S'} \<le> \<Sum> ?S'"
       using Suc by (intro Suc; auto)
 
     hence "\<Sum> {0..<card ?S'} + x \<le> \<Sum> ?S' + Max S"
-      using `Max S \<ge> x` by simp
+      using \<open>Max S \<ge> x\<close> by simp
     also have "... = \<Sum> S"
-      using sum.remove[OF `finite S` `Max S \<in> S`, where g="\<lambda>x. x"]
+      using sum.remove[OF \<open>finite S\<close> \<open>Max S \<in> S\<close>, where g="\<lambda>x. x"]
       by simp
     finally show ?case
       using cards Suc by auto