--- a/src/HOL/IMP/BExp.thy Sun Oct 23 14:03:37 2011 +0200
+++ b/src/HOL/IMP/BExp.thy Sun Oct 23 14:15:24 2011 +0200
@@ -72,10 +72,10 @@
text_raw{*\begin{isaverbatimwrite}\newcommand{\BExpbsimpdef}{% *}
fun bsimp :: "bexp \<Rightarrow> bexp" where
-"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)" |
+"bsimp (Bc v) = Bc v" |
+"bsimp (Not b) = not(bsimp b)" |
"bsimp (And b\<^isub>1 b\<^isub>2) = and (bsimp b\<^isub>1) (bsimp b\<^isub>2)" |
-"bsimp (Not b) = not(bsimp b)" |
-"bsimp (Bc v) = Bc v"
+"bsimp (Less a\<^isub>1 a\<^isub>2) = less (asimp a\<^isub>1) (asimp a\<^isub>2)"
text_raw{*}\end{isaverbatimwrite}*}
value "bsimp (And (Less (N 0) (N 1)) b)"