src/Doc/Tutorial/Datatype/unfoldnested.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
equal deleted inserted replaced
58859:d5ff8b782b29 58860:fee7cfa69c50
     1 (*<*)
     1 (*<*)
     2 theory unfoldnested imports Main begin;
     2 theory unfoldnested imports Main begin
     3 (*>*)
     3 (*>*)
     4 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
     4 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
     5 and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
     5 and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
     6 (*<*)
     6 (*<*)
     7 end
     7 end