changeset 10971 | 6852682eaf16 |
parent 8751 | 9ed0548177fb |
child 16417 | 9bc16273c2d4 |
--- a/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 11:59:15 2001 +0100 +++ b/doc-src/TutorialI/Datatype/unfoldnested.thy Wed Jan 24 12:29:10 2001 +0100 @@ -1,8 +1,8 @@ (*<*) theory unfoldnested = Main:; (*>*) -datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term_list" -and ('a,'b)term_list = Nil | Cons "('a,'b)term" "('a,'b)term_list" +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list" +and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list" (*<*) end (*>*)