doc-src/TutorialI/Datatype/unfoldnested.thy
author haftmann
Thu, 16 Jun 2005 10:22:50 +0200
changeset 16405 0a2a6732c685
parent 10971 6852682eaf16
child 16417 9bc16273c2d4
permissions -rw-r--r--
added macos emacs hints

(*<*)
theory unfoldnested = Main:;
(*>*)
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
(*>*)