changeset 72991 | d0a0b74f0ad7 |
parent 69605 | a96320074298 |
72990:db8f94656024 | 72991:d0a0b74f0ad7 |
---|---|
1 (*<*)theory Even imports Main begin |
1 (*<*)theory Even imports "../Setup" begin(*>*) |
2 ML_file \<open>../../antiquote_setup.ML\<close> |
|
3 (*>*) |
|
4 |
2 |
5 section\<open>The Set of Even Numbers\<close> |
3 section\<open>The Set of Even Numbers\<close> |
6 |
4 |
7 text \<open> |
5 text \<open> |
8 \index{even numbers!defining inductively|(}% |
6 \index{even numbers!defining inductively|(}% |