# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719482352 -7200
# Node ID 89c20f7f3b3bc81f9b1330a755fb8e844d96342f
# Parent  4b10ae56ed01c73fb23a299eb301e8584d7bd539
tuned comment;

diff -r 4b10ae56ed01 -r 89c20f7f3b3b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 27 09:41:16 2024 +0200
+++ b/src/HOL/List.thy	Thu Jun 27 11:59:12 2024 +0200
@@ -182,7 +182,7 @@
 "find P (x#xs) = (if P x then Some x else find P xs)"
 
 text \<open>In the context of multisets, \<open>count_list\<close> is equivalent to
-  \<^term>\<open>count \<circ> mset\<close> and it it advisable to use the latter.\<close>
+  \<^term>\<open>count \<circ> mset\<close> and it is advisable to use the latter.\<close>
 primrec count_list :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where
 "count_list [] y = 0" |
 "count_list (x#xs) y = (if x=y then count_list xs y + 1 else count_list xs y)"