src/HOL/Word/Word.thy
changeset 70901 94a0c47b8553
parent 70900 954e7f79c25a
child 71149 a7d1fb0c9e16
--- a/src/HOL/Word/Word.thy	Fri Oct 18 18:41:31 2019 +0000
+++ b/src/HOL/Word/Word.thy	Fri Oct 18 18:41:33 2019 +0000
@@ -286,6 +286,12 @@
 
 end
 
+quickcheck_generator word
+  constructors:
+    "zero_class.zero :: ('a::len) word",
+    "numeral :: num \<Rightarrow> ('a::len) word",
+    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"
+
 text \<open>Legacy theorems:\<close>
 
 lemma word_arith_wis [code]: