# HG changeset patch
# User wenzelm
# Date 1350567854 -7200
# Node ID 18af317f393aef21f35b796b73fc4552c7dbc0c8
# Parent  26a0263f9f4681ddc9a5ad20e9c35f396de72df7# Parent  12cece6d951da368db249841da93f35b06ba4e4b
merged

diff -r 12cece6d951d -r 18af317f393a src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Thu Oct 18 15:28:49 2012 +0200
+++ b/src/HOL/IMP/BExp.thy	Thu Oct 18 15:44:14 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)