# HG changeset patch
# User nipkow
# Date 1430727733 -7200
# Node ID 031ec3d34d3192ca9decf95392caff0b119786dc
# Parent  5ef8ed6859659510fd5420a6af5859bc422effb4
no longer needed

diff -r 5ef8ed685965 -r 031ec3d34d31 src/HOL/IMP/BExp.thy
--- 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: *}