--- a/src/HOL/SMT/Examples/SMT_Examples.thy Fri Nov 06 14:42:42 2009 +0100 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy Fri Nov 06 17:52:57 2009 +0100 @@ -549,7 +549,7 @@ section {* Bitvectors *} -locale bv +locale z3_bv_test begin text {*