| changeset 58860 | fee7cfa69c50 |
| parent 48985 | 5386df44a037 |
| 58859:d5ff8b782b29 | 58860:fee7cfa69c50 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory unfoldnested imports Main begin; |
2 theory unfoldnested imports Main begin |
3 (*>*) |
3 (*>*) |
4 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list" |
4 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list" |
5 and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list" |
5 and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list" |
6 (*<*) |
6 (*<*) |
7 end |
7 end |