53 and 'a branch = Branch 'a "'a tree'" |
53 and 'a branch = Branch 'a "'a tree'" |
54 |
54 |
55 datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
55 datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
56 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
56 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
57 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
57 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
|
58 |
|
59 datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree" |
58 |
60 |
59 datatype_new ('a, 'b, 'c) some_killing = |
61 datatype_new ('a, 'b, 'c) some_killing = |
60 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
62 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
61 and ('a, 'b, 'c) in_here = |
63 and ('a, 'b, 'c) in_here = |
62 IH1 'b 'a | IH2 'c |
64 IH1 'b 'a | IH2 'c |