--- 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])"