doc-src/TutorialI/Datatype/unfoldnested.thy
author wenzelm
Thu, 01 Oct 2009 20:06:11 +0200
changeset 32834 a4e0b8d88f28
parent 16417 9bc16273c2d4
permissions -rw-r--r--
avoid unsynchronized refs within theory sources;

(*<*)
theory unfoldnested imports Main begin;
(*>*)
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
(*>*)