src/HOL/Data_Structures/Tree23.thy
changeset 61679 1335462046e8
parent 61640 44c9198f210c
child 66302 fd89f97c80c2
equal deleted inserted replaced
61678:b594e9277be3 61679:1335462046e8
     8 
     8 
     9 class height =
     9 class height =
    10 fixes height :: "'a \<Rightarrow> nat"
    10 fixes height :: "'a \<Rightarrow> nat"
    11 
    11 
    12 datatype 'a tree23 =
    12 datatype 'a tree23 =
    13   Leaf |
    13   Leaf ("\<langle>\<rangle>") |
    14   Node2 "'a tree23" 'a "'a tree23" |
    14   Node2 "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _\<rangle>") |
    15   Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"
    15   Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _, _, _\<rangle>")
    16 
    16 
    17 fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
    17 fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
    18 "inorder Leaf = []" |
    18 "inorder Leaf = []" |
    19 "inorder(Node2 l a r) = inorder l @ a # inorder r" |
    19 "inorder(Node2 l a r) = inorder l @ a # inorder r" |
    20 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
    20 "inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"