changeset 45216 | a51a70687517 |
parent 45200 | 1f1897ac7877 |
child 45255 | ffc06165d272 |
--- a/src/HOL/IMP/BExp.thy Thu Oct 20 09:48:00 2011 +0200 +++ b/src/HOL/IMP/BExp.thy Thu Oct 20 10:43:47 2011 +0200 @@ -5,7 +5,7 @@ datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where -"bval (Bc v) _ = v" | +"bval (Bc v) s = v" | "bval (Not b) s = (\<not> bval b s)" | "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"