# HG changeset patch
# User haftmann
# Date 1571424093 0
# Node ID 94a0c47b8553a9b9ba7e1df56dfce16ec5ab4d76
# Parent  954e7f79c25a1ea2003c1389e8f5e814dbaa6148
moved quickcheck setup to distribution

diff -r 954e7f79c25a -r 94a0c47b8553 src/HOL/Library/Type_Length.thy
--- a/src/HOL/Library/Type_Length.thy	Fri Oct 18 18:41:31 2019 +0000
+++ b/src/HOL/Library/Type_Length.thy	Fri Oct 18 18:41:33 2019 +0000
@@ -70,4 +70,37 @@
 instance bit1 :: (len0) len
   by standard simp
 
+instantiation Enum.finite_1 :: len
+begin
+
+definition
+  "len_of_finite_1 (x :: Enum.finite_1 itself) \<equiv> (1 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_1_def)
+
 end
+
+instantiation Enum.finite_2 :: len
+begin
+
+definition
+  "len_of_finite_2 (x :: Enum.finite_2 itself) \<equiv> (2 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_2_def)
+
+end
+
+instantiation Enum.finite_3 :: len
+begin
+
+definition
+  "len_of_finite_3 (x :: Enum.finite_3 itself) \<equiv> (4 :: nat)"
+
+instance
+  by standard (auto simp: len_of_finite_3_def)
+
+end
+
+end
diff -r 954e7f79c25a -r 94a0c47b8553 src/HOL/Word/Word.thy
--- 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]: