# HG changeset patch
# User nipkow
# Date 1350567602 -7200
# Node ID 26a0263f9f4681ddc9a5ad20e9c35f396de72df7
# Parent  54ec43352eb1c790a7c220b620186248329610ca
tuned

diff -r 54ec43352eb1 -r 26a0263f9f46 src/HOL/IMP/BExp.thy
--- 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)