changeset 63167 | 0909deb8059b |
parent 61076 | bdc1e2f0a86a |
child 74641 | 6f801e1073fa |
63166:143f58bb34f9 | 63167:0909deb8059b |
---|---|
3 Copyright 2009-2011 |
3 Copyright 2009-2011 |
4 |
4 |
5 Examples featuring Nitpick's "specialize" optimization. |
5 Examples featuring Nitpick's "specialize" optimization. |
6 *) |
6 *) |
7 |
7 |
8 section {* Examples Featuring Nitpick's \textit{specialize} Optimization *} |
8 section \<open>Examples Featuring Nitpick's \textit{specialize} Optimization\<close> |
9 |
9 |
10 theory Special_Nits |
10 theory Special_Nits |
11 imports Main |
11 imports Main |
12 begin |
12 begin |
13 |
13 |