Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
isabelle update_cartouches;
authorwenzelm
Fri, 08 Jan 2021 15:13:23 +0100
changeset 73102 87067698ae53
parent 73101 3d5d949cd865
child 73103 b69fd6e19662
child 73105 578a33042aa6
isabelle update_cartouches;
src/HOL/Algebra/Multiplicative_Group.thy file | annotate | diff | comparison | revisions
src/HOL/Lattices_Big.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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)
   {
isabelle