no longer needed

--- a/src/HOL/IMP/BExp.thy	Sun May 03 15:38:25 2015 +0200
+++ b/src/HOL/IMP/BExp.thy	Mon May 04 10:22:13 2015 +0200
@@ -16,15 +16,6 @@
             <''x'' := 3, ''y'' := 1>"
 
 
-text{* To improve automation: *}
-
-lemma bval_And_if[simp]:
-  "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)"
-by(simp)
-
-declare bval.simps(3)[simp del]  --"remove the original eqn"
-
-
 subsection "Constant Folding"
 
 text{* Optimizing constructors: *}