changeset 14800 | 50581f2b2c0e |
parent 14443 | 75910c7557c5 |
--- a/src/HOL/Numeral.thy Fri May 21 21:48:03 2004 +0200 +++ b/src/HOL/Numeral.thy Fri May 21 21:48:35 2004 +0200 @@ -109,8 +109,8 @@ bin_add_Min: "bin_add bin.Min w = bin_pred w" bin_add_BIT: "bin_add (v BIT x) w = - (case w of Pls => v BIT x - | Min => bin_pred (v BIT x) + (case w of bin.Pls => v BIT x + | bin.Min => bin_pred (v BIT x) | (w BIT y) => NCons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y))"