54 data ('a, 'b, 'c) some_killing = |
54 data ('a, 'b, 'c) some_killing = |
55 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
55 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
56 and ('a, 'b, 'c) in_here = |
56 and ('a, 'b, 'c) in_here = |
57 IH1 'b 'a | IH2 'c |
57 IH1 'b 'a | IH2 'c |
58 |
58 |
59 data 'b nofail1 = NF11 "'b nofail1 \<times> 'b" | NF12 'b |
59 data 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b |
60 data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" |
60 data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" |
61 data 'b nofail3 = NF3 "'b \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" |
61 data 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" |
62 data 'b nofail4 = NF4 "('b nofail3 \<times> ('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset) list" |
62 data 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list" |
63 |
63 |
64 (* |
64 (* |
65 data 'b fail = F "'b fail \<times> 'b \<times> 'b fail \<times> 'b list" |
65 data 'b fail = F "'b fail" 'b "'b fail" "'b list" |
66 data 'b fail = F "'b fail \<times> 'b \<times> 'b fail \<times> 'b" |
66 data 'b fail = F "'b fail" 'b "'b fail" 'b |
67 data 'b fail = F "'b fail \<times> 'b + 'b fail" |
67 data 'b fail = F1 "'b fail" 'b | F2 "'b fail" |
68 data 'b fail = F "'b fail \<times> 'b" |
68 data 'b fail = F "'b fail" 'b |
69 *) |
69 *) |
70 |
70 |
71 data l1 = L1 "l2 list" |
71 data l1 = L1 "l2 list" |
72 and l2 = L21 "l1 fset" | L22 l2 |
72 and l2 = L21 "l1 fset" | L22 l2 |
73 |
73 |