
diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/Adder.thy
--- a/src/HOL/ex/Adder.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Adder.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -15,7 +15,7 @@
   by (cases bv) (simp_all add: bv_to_nat_helper)
 
 definition
-  half_adder :: "[bit, bit] => bit list"
+  half_adder :: "[bit, bit] => bit list" where
   "half_adder a b = [a bitand b, a bitxor b]"
 
 lemma half_adder_correct: "bv_to_nat (half_adder a b) = bitval a + bitval b"
@@ -28,7 +28,7 @@
   by (simp add: half_adder_def)
 
 definition
-  full_adder :: "[bit, bit, bit] => bit list"
+  full_adder :: "[bit, bit, bit] => bit list" where
   "full_adder a b c =
       (let x = a bitxor b in [a bitand b bitor c bitand x, x bitxor c])"
 




