src/Doc/Tutorial/Datatype/unfoldnested.thy
author desharna
Sun, 28 Nov 2021 19:15:12 +0100
changeset 74869 7b0a241732c1
parent 58860 fee7cfa69c50
permissions -rw-r--r--
added definitions multp{DM,HO} and corresponding lemmas

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