Adapted to new syntax for case expressions.
authorberghofe
Fri, 21 May 2004 21:48:35 +0200
changeset 14800 50581f2b2c0e
parent 14799 a405aadff16c
child 14801 2d27b5ebc447
Adapted to new syntax for case expressions.
src/HOL/Numeral.thy
--- 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))"