# HG changeset patch
# User paulson
# Date 1675960193 0
# Node ID 268c8184288349b4e755c9d78575051edd57ecc3
# Parent  b6f3eb537d912c913dfc3eac7c927d14434e530a# Parent  8c093a4b8ccf9a9628cfd771504963c1944e1c7c
merged

diff -r 8c093a4b8ccf -r 268c81842883 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Thu Feb 09 15:36:06 2023 +0000
+++ b/src/HOL/Library/Word.thy	Thu Feb 09 16:29:53 2023 +0000
@@ -605,20 +605,21 @@
   where \<open>enum_word = map word_of_nat [0..<2 ^ LENGTH('a)]\<close>
 
 definition enum_all_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
-  where \<open>enum_all_word = Ball UNIV\<close>
+  where \<open>enum_all_word = All\<close>
 
 definition enum_ex_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
-  where \<open>enum_ex_word = Bex UNIV\<close>
+  where \<open>enum_ex_word = Ex\<close>
+
+instance
+  by standard
+    (simp_all add: enum_all_word_def enum_ex_word_def enum_word_def distinct_map inj_on_word_of_nat flip: UNIV_word_eq_word_of_nat)
+
+end
 
 lemma [code]:
-  \<open>Enum.enum_all P \<longleftrightarrow> Ball UNIV P\<close>
-  \<open>Enum.enum_ex P \<longleftrightarrow> Bex UNIV P\<close> for P :: \<open>'a word \<Rightarrow> bool\<close>
-  by (simp_all add: enum_all_word_def enum_ex_word_def)
-
-instance
-  by standard (simp_all add: UNIV_word_eq_word_of_nat inj_on_word_of_nat enum_word_def enum_all_word_def enum_ex_word_def distinct_map)
-
-end
+  \<open>Enum.enum_all P \<longleftrightarrow> list_all P Enum.enum\<close>
+  \<open>Enum.enum_ex P \<longleftrightarrow> list_ex P Enum.enum\<close> for P :: \<open>'a::len word \<Rightarrow> bool\<close>
+  by (simp_all add: enum_all_word_def enum_ex_word_def enum_UNIV list_all_iff list_ex_iff)
 
 
 subsection \<open>Bit-wise operations\<close>