equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Nested1 = Nested0:; |
2 theory Nested1 = Nested0:; |
3 (*>*) |
3 (*>*) |
4 consts trev :: "('a,'b)term \<Rightarrow> ('a,'b)term"; |
|
5 |
4 |
6 text{*\noindent |
5 text{*\noindent |
7 Although the definition of @{term trev} is quite natural, we will have |
6 Although the definition of @{term trev} is quite natural, we will have |
8 overcome a minor difficulty in convincing Isabelle of is termination. |
7 overcome a minor difficulty in convincing Isabelle of is termination. |
9 It is precisely this difficulty that is the \textit{raison d'\^etre} of |
8 It is precisely this difficulty that is the \textit{raison d'\^etre} of |