--- a/src/HOL/Import/HOL/HOL4Vec.thy Sat Feb 16 16:52:09 2008 +0100
+++ b/src/HOL/Import/HOL/HOL4Vec.thy Sun Feb 17 06:49:53 2008 +0100
@@ -1283,9 +1283,8 @@
(op -->::bool => bool => bool)
((op <::nat => nat => bool) x
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit))))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int) (Int.Pls \<Colon> int)))))
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
x))"
by (import bword_num BV_VB)
@@ -1500,10 +1499,9 @@
((BV::bool => nat) cin))
((op ^::nat => nat => nat)
((number_of \<Colon> int => nat)
- ((op BIT \<Colon> int => bit => int)
- ((op BIT \<Colon> int => bit => int)
- (Int.Pls \<Colon> int) (bit.B1::bit))
- (bit.B0::bit)))
+ ((Int.Bit0 \<Colon> int => int)
+ ((Int.Bit1 \<Colon> int => int)
+ (Int.Pls \<Colon> int))))
k)))))))"
by (import bword_arith ACARRY_EQ_ADD_DIV)