author | berghofe |
Fri, 21 May 2004 21:48:35 +0200 | |
changeset 14800 | 50581f2b2c0e |
parent 14799 | a405aadff16c |
child 14801 | 2d27b5ebc447 |
--- 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))"