| changeset 16417 | 9bc16273c2d4 |
| parent 15905 | 0a4cc9b113c7 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Nested1 = Nested0: |
2 theory Nested1 imports Nested0 begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent |
5 text{*\noindent |
6 Although the definition of @{term trev} below is quite natural, we will have |
6 Although the definition of @{term trev} below is quite natural, we will have |
7 to overcome a minor difficulty in convincing Isabelle of its termination. |
7 to overcome a minor difficulty in convincing Isabelle of its termination. |