doc-src/TutorialI/Datatype/unfoldnested.thy
author nipkow
Wed, 19 Apr 2000 13:40:42 +0200
changeset 8751 9ed0548177fb
child 10971 6852682eaf16
permissions -rw-r--r--
*** empty log message ***

(*<*)
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"
(*<*)
end
(*>*)