| changeset 41413 | 64cd30d6b0b8 |
| parent 39246 | 9e58f0499f57 |
| child 47108 | 2a1953f0d20d |
| 41412:35f30e07fe0d | 41413:64cd30d6b0b8 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Examples for generic reflection and reification *} |
5 header {* Examples for generic reflection and reification *} |
6 |
6 |
7 theory ReflectionEx |
7 theory ReflectionEx |
8 imports Reflection |
8 imports "~~/src/HOL/Library/Reflection" |
9 begin |
9 begin |
10 |
10 |
11 text{* This theory presents two methods: reify and reflection *} |
11 text{* This theory presents two methods: reify and reflection *} |
12 |
12 |
13 text{* |
13 text{* |