equal
deleted
inserted
replaced
107 primrec |
107 primrec |
108 bin_add_Pls: "bin_add bin.Pls w = w" |
108 bin_add_Pls: "bin_add bin.Pls w = w" |
109 bin_add_Min: "bin_add bin.Min w = bin_pred w" |
109 bin_add_Min: "bin_add bin.Min w = bin_pred w" |
110 bin_add_BIT: |
110 bin_add_BIT: |
111 "bin_add (v BIT x) w = |
111 "bin_add (v BIT x) w = |
112 (case w of Pls => v BIT x |
112 (case w of bin.Pls => v BIT x |
113 | Min => bin_pred (v BIT x) |
113 | bin.Min => bin_pred (v BIT x) |
114 | (w BIT y) => |
114 | (w BIT y) => |
115 NCons (bin_add v (if (x & y) then bin_succ w else w)) |
115 NCons (bin_add v (if (x & y) then bin_succ w else w)) |
116 (x~=y))" |
116 (x~=y))" |
117 |
117 |
118 primrec |
118 primrec |