tuned

--- a/src/HOL/IMP/BExp.thy	Thu Oct 18 15:10:49 2012 +0200
+++ b/src/HOL/IMP/BExp.thy	Thu Oct 18 15:40:02 2012 +0200
@@ -80,7 +80,7 @@
 
 value "bsimp (And (Less (N 0) (N 1)) b)"
 
-value "bsimp (And (Less (N 1) (N 0)) (B True))"
+value "bsimp (And (Less (N 1) (N 0)) (Bc True))"
 
 theorem "bval (bsimp b) s = bval b s"
 apply(induction b)