equal
deleted
inserted
replaced
15 you needed to reprove many lemmas reminiscent of similar lemmas about |
15 you needed to reprove many lemmas reminiscent of similar lemmas about |
16 @{term"rev"}. We will now show you how \isacommand{recdef} can simplify |
16 @{term"rev"}. We will now show you how \isacommand{recdef} can simplify |
17 definitions and proofs about nested recursive datatypes. As an example we |
17 definitions and proofs about nested recursive datatypes. As an example we |
18 choose exercise~\ref{ex:trev-trev}: |
18 choose exercise~\ref{ex:trev-trev}: |
19 *} |
19 *} |
20 (* consts trev :: "('a,'b)term => ('a,'b)term" *) |
20 |
21 (*<*) |
21 consts trev :: "('a,'b)term \<Rightarrow> ('a,'b)term" |
22 end |
22 (*<*)end(*>*) |
23 (*>*) |
|