# HG changeset patch
# User wenzelm
# Date 1610115203 -3600
# Node ID 87067698ae53d5e97f95ffbd370d3408a9ccd964
# Parent  3d5d949cd865cd5558b10ad5a944495c6e8055b5
isabelle update_cartouches;

diff -r 3d5d949cd865 -r 87067698ae53 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jan 08 15:07:25 2021 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Fri Jan 08 15:13:23 2021 +0100
@@ -668,7 +668,7 @@
     unfolding subgroup_generated_def
     using a by simp
   then show ?thesis
-    using `ord a = 0` by auto
+    using \<open>ord a = 0\<close> by auto
 next
   case False
   note finite_subgroup = this
diff -r 3d5d949cd865 -r 87067698ae53 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Fri Jan 08 15:07:25 2021 +0100
+++ b/src/HOL/Lattices_Big.thy	Fri Jan 08 15:13:23 2021 +0100
@@ -744,7 +744,7 @@
   assumes "P {}" 
   assumes "\<And>x S. finite S \<Longrightarrow> (\<And>y. y \<in> S \<Longrightarrow> f y \<le> f x) \<Longrightarrow> P S \<Longrightarrow> P (insert x S)"
   shows "P S"
-  using `finite S` 
+  using \<open>finite S\<close> 
 proof (induction rule: finite_psubset_induct)
   case (psubset A)
   {