equal
deleted
inserted
replaced
15 "HOL-Computational_Algebra.Polynomial_Factorial" |
15 "HOL-Computational_Algebra.Polynomial_Factorial" |
16 "HOL-Number_Theory.Eratosthenes" |
16 "HOL-Number_Theory.Eratosthenes" |
17 "HOL-ex.Records" |
17 "HOL-ex.Records" |
18 begin |
18 begin |
19 |
19 |
20 text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
20 text \<open>Drop technical stuff from @{theory HOL.Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
21 |
21 |
22 setup \<open> |
22 setup \<open> |
23 fn thy => |
23 fn thy => |
24 let |
24 let |
25 val tycos = Sign.logical_types thy; |
25 val tycos = Sign.logical_types thy; |