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]: