equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section \<open>Examples for code generation timing measures\<close> |
5 section \<open>Examples for code generation timing measures\<close> |
6 |
6 |
7 theory Code_Timing |
7 theory Code_Timing |
8 imports "~~/src/HOL/Number_Theory/Eratosthenes" |
8 imports "HOL-Number_Theory.Eratosthenes" |
9 begin |
9 begin |
10 |
10 |
11 declare [[code_timing]] |
11 declare [[code_timing]] |
12 |
12 |
13 definition primes_upto :: "nat \<Rightarrow> int list" |
13 definition primes_upto :: "nat \<Rightarrow> int list" |