changeset 72025 | b4ed07cbe954 |
parent 69597 | ff784d5a5bfb |
child 72029 | 83456d9f0ed5 |
--- a/src/HOL/Codegenerator_Test/Candidates.thy Sat Jul 11 18:09:09 2020 +0000 +++ b/src/HOL/Codegenerator_Test/Candidates.thy Sun Jul 12 18:10:06 2020 +0000 @@ -16,6 +16,7 @@ "HOL-Computational_Algebra.Polynomial_Factorial" "HOL-Number_Theory.Eratosthenes" "HOL-ex.Records" + "HOL-Word.Word" begin text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>