60  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"

    60  "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2"

    61 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"

    61 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2"

    62 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"

    62 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"

    63 | "\<turnstile> Void : EMPTY"

    63 | "\<turnstile> Void : EMPTY"

    64 | "\<turnstile> Char c : CHAR c"

    64 | "\<turnstile> Char c : CHAR c"

    65 

    67 

    66 section {* The string behind a value *}

    68 section {* The string behind a value *}

    67 

    69 

    68 fun flat :: "val \<Rightarrow> string"

    70 fun flat :: "val \<Rightarrow> string"

    69 where

    71 where