changeset 42142 | d24a93025feb |
parent 41413 | 64cd30d6b0b8 |
child 42187 | b4f4ed5b8586 |
42141:2c255ba8f299 | 42142:d24a93025feb |
---|---|
1 theory Specialisation_Examples |
1 theory Specialisation_Examples |
2 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
2 imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs" |
3 begin |
3 begin |
4 |
|
5 declare [[values_timeout = 240.0]] |
|
4 |
6 |
5 section {* Specialisation Examples *} |
7 section {* Specialisation Examples *} |
6 |
8 |
7 primrec nth_el' |
9 primrec nth_el' |
8 where |
10 where |